Skip to content

proof(L1.G): strengthen T_Var_*_L1 with region well-formedness (§4.8 path 3)#170

Merged
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l1g-strengthen-var-rules
May 27, 2026
Merged

proof(L1.G): strengthen T_Var_*_L1 with region well-formedness (§4.8 path 3)#170
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l1g-strengthen-var-rules

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Lands resolution path 3 from formal/PRESERVATION-DESIGN.md §4.8 — strengthens T_Var_Lin_L1 / T_Var_Unr_L1 with the premise

forall r, In r (free_regions T) -> In r R

closing the source-level soundness gap where a variable of type TString r could be used at an R no longer containing r. Stacked onto the L1 umbrella PR #153.

What this PR does

  • formal/TypingL1.v — strengthens both variable rules; header comment links to §4.8 resolution path 3.
  • formal/Semantics_L1.v — fixes the hypothesis renumbering (the new well-formedness premise lands at H1 for both rules) via explicit rename H1 into Hwf + threading through T_Var_*_L1 applications. Touches shift_typing_gen_l1 and subst_typing_gen_l1. The existing region_shrink_preserves_typing_l1_gen gains two T_Var-case admits (joining the existing two T_Region-case admits — that lemma is already Admitted); the wrapper region_shrink_preserves_typing_l1 is unchanged.
  • formal/PRESERVATION-DESIGN.md §4.8.1 — new sub-section records the landing and the residual axiom obstacle.

What this PR does NOT do — and why

It does not close Axiom region_liveness_at_split_l1. An empirical closure attempt (replacing Axiom with Lemma, doing structural induction) shows 23 of 25 cases close trivially via IH chains, but T_Region_Active_L1 with binder=rv remains a genuine obstacle even under the strengthened judgment. Minimal counterexample at the typing level:

ERegion rv (EI32 5) : TBase TI32 -| []  at  R = [rv]

The rule pops the only rv on exit, so In rv R' is false. The axiom's in-source header (Semantics_L1.v around L895) now documents this finding with three follow-up closure paths (side-conditioned lemma, multi-set R, contextual weaker signature). Closing it is L1 follow-up work — independent of, and additional to, this §4.8 resolution.

Counterexample regression

bad_input_untypable_l1 in Counterexample.v still closes Qed. — that proof inverts T_Pair_L1 / T_Loc_L1 / T_Region_*_L1, not T_Var_*_L1, so the strengthening is orthogonal.

Test plan

  • cd formal && coq_makefile -f _CoqProject -o build.mk && make -f build.mk -j2 — clean rebuild green (~31s, coqc 8.18.0)
  • Counterexample.v still Qed on bad_input_untypable_l1
  • Semantics_L1.v still Qed on the 22 lemmas that were Qed pre-PR
  • No new admits in Semantics.v (legacy judgment untouched)
  • Empirical closure attempt of region_liveness_at_split_l1 ran; 23/25 cases via IH chains, T_Region_Active_L1 obstacle confirmed

🤖 Generated with Claude Code

…path 3)

Adds the premise `forall r, In r (free_regions T) -> In r R` to
T_Var_Lin_L1 and T_Var_Unr_L1, the third resolution path from
PRESERVATION-DESIGN.md §4.8 (T_Var_*_L1 too permissive about region
presence). With the strengthening, programs that bind a linear
TString r variable and then use it after a region scope has popped
r — operationally a dangling reference — no longer type:

  let_lin x = (ELoc 0 "r") in
    (ELet (ERegion "r" (EI32 5)) (EDrop (EVar 1)))

  fails at the EDrop site: R has been popped to [] and the
  strengthened T_Var_Lin_L1 requires In "r" R for x : TString "r".

What landed:
- TypingL1.v: T_Var_Lin_L1 and T_Var_Unr_L1 gain the well-formedness
  premise. Header documents the link to §4.8 resolution path 3.
- Semantics_L1.v: existing proofs that destructured H1 (the
  auto-name now bound to the new well-formedness premise) get
  explicit `rename H1 into Hwf` + threading through `T_Var_*_L1`
  applications. region_shrink_preserves_typing_l1_gen gains two
  T_Var-case admits, joining the existing two T_Region-case admits;
  the file remains compilable and the wrapper
  region_shrink_preserves_typing_l1 is unchanged.
- Counterexample.v: bad_input_untypable_l1 still closes (Qed),
  doesn't depend on T_Var_*_L1.

What this PR does NOT do:
- Close `region_liveness_at_split_l1`. An empirical closure attempt
  (Axiom → Lemma, structural induction) closes 23 of 25 cases via
  IH chains, but T_Region_Active_L1 with binder=rv remains a real
  obstacle even under the strengthened judgment. The minimal
  counterexample is `ERegion rv (EI32 5)` at R = [rv]: typed at
  TBase TI32, R' = [] via remove_first_L1, so the axiom's
  conclusion `In rv R'` is false. The axiom's in-source header
  (Semantics_L1.v ~L895) now documents this with three follow-up
  closure paths (side-conditioned lemma, multi-set R,
  contextual weaker signature).
- Modify any of the 22 Qed proofs in Semantics_L1.v beyond
  hypothesis renaming.
- Touch Semantics.v (legacy judgment) or operational semantics.

PRESERVATION-DESIGN.md §4.8.1 records the landing + the residual
axiom obstacle.

Validation: clean rebuild green in ~31s (coqc 8.18.0).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 0356a74 into proof/l1-region-threading-design May 27, 2026
0 of 8 checks passed
@hyperpolymath hyperpolymath deleted the proof/l1g-strengthen-var-rules branch May 27, 2026 09:56
hyperpolymath added a commit that referenced this pull request May 27, 2026
…-layer dependency) (#172)

## Summary

Adds a new sub-section **§5.1** to `formal/PRESERVATION-DESIGN.md`
documenting how L1's open lambda-rigidity admits (`S_App_Step2` /
`S_Pair_Step2` in `preservation_l1`) close at the L2 layer via
effect-typed `TFun`, not at L1 directly.

## Why this matters

The §5 preservation table currently reads:

| Property | Ephapax-Linear |
|---|---|
| Preservation | ✓ (L1 fix) |

…but `preservation_l1` is `Admitted` and §4.8 documents the
lambda-rigidity gap as one of three independent resolution paths. §4.8.1
(added by PR #170) records that path (3) — `T_Var_*_L1` strengthening —
has landed, but explicitly notes it leaves the lambda-body case open.

There's nowhere in the doc that connects §4.8 path (1) — *effect-typed
lambdas* — to the L2 layer. Readers of §5 see "✓ (L1 fix)" without
knowing the closure is conditional on L2 phase-2 work.

## What §5.1 adds

- The "✓ (L1 fix)" cell flagged with `(*conditional on §5.1*)`.
- Honest read of what L1 closes today (`S_StringConcat_Step2` tractable;
`S_App_Step2` / `S_Pair_Step2` L2-gated).
- Why path (3) (T_Var strengthening) is necessary-not-sufficient.
- Concrete proposed effect-typed `TFun` signature (region-in /
region-out as parameters).
- Why L2 is the natural home (effect-typing is a typing-layer concern,
not a region-layer one).
- Sequencing: planned as L2 Phase 2 after the current `TypingL2.v`
skeleton (#168).

## Branch base

Stacked off `proof/l1-region-threading-design` (head `0356a74`, post-PR
#170). Will rebase to `main` when #153 lands.

## Test plan

- [x] Asciidoc / Markdown lints (the file is Markdown so AsciiDoc
tooling skipped)
- [x] Cross-references to §4.8 / §4.8.1 verified to match current doc
structure
- [ ] Review: §5.1 should integrate cleanly with §4.8 / §4.8.1; the
"effect-typed TFun" sketch is a *direction*, not a proposed final
signature — final shape is L2 Phase 2's call

Refs PRESERVATION-DESIGN.md §4.8 + §4.8.1, PR #153, PR #168, PR #170.

🤖 Generated with [Claude Code](https://claude.com/claude-code)
hyperpolymath added a commit that referenced this pull request May 27, 2026
…ervation patching (#175)

## Summary

Owner directive 2026-05-27 (received during a session that had just
shipped PR #170 doing exactly the patching the directive forbids):

> We are no longer treating preservation as a proof-engineering problem.
… Do not optimize for smallest patch size. Make sure that never happens
again, and it is very clear what the work is wherever needs documenting;
no further time can be spent on the 'old approach'.

This PR makes the directive impossible to miss across every doc surface
an agent (or human) might encounter when picking up \`formal/\` work.

## What this changes

### NEW: \`CLAUDE.md\` at repo root

Agent-facing guidance with:
- 60-second TL;DR of why preservation in \`Semantics.v\` cannot be
closed.
- Explicit **DO NOT** list (5 items): no closing legacy preservation, no
extending \`Semantics.v\` with closure-supporting lemmas, no closing
\`region_liveness_at_split_l1\` axiom via proof tricks, no following
pre-2026-05-26 closure plans, no patching legacy \`Typing.v\`.
- Affirmative path: read \`PRESERVATION-DESIGN.md\` first; work proceeds
per-layer (L1 / L2 / L3 / L4).
- File reference table marking each \`formal/*.v\` as legacy-frozen vs
active-layered vs forward-looking.
- Two diagnostic questions to ask before touching \`formal/\`.

### Banner: \`formal/PRESERVATION-DESIGN.md\`

CANONICAL banner at top. Same 4-item anti-pattern list as CLAUDE.md plus
the **anti-pattern detector**: "if a session is producing
sibling-region-disjointness side conditions, region-weakening predicates
indexed on syntactic shape, or admit-shuffling between Semantics.v and a
new lemma — escalate to a layer-design discussion."

### Banner: \`formal/PRESERVATION-HANDOFF.md\`

Strengthened from "Superseded" to "ARCHAEOLOGY ONLY — do NOT follow the
closure plans in this file." Keeps the historical 910→12 reduction data
for diagnostic value but explicitly marks it not-a-plan.

### Surgery: \`ROADMAP.adoc\`

- v0.1 "Coq: close preservation to Qed" checkbox rewritten in layered
terms (the work is per-layer derivation, not legacy-theorem closure).
- The 230-line **§ Preservation closure plan** body (5 phases, all aimed
at closing the falsified theorem) is removed. Git history retains it for
forensic value.
- Replaced with a brief "superseded by four-layer redesign" section
pointing at the design doc + CLAUDE.md.

### Memory store


\`~/.claude/.../memory/feedback_ephapax_no_patching_legacy_preservation.md\`
captures the durable directive. The \`MEMORY.md\` index surfaces it in
the always-on disambiguation block alongside the existing
ephapax/affinescript disambiguation entry so future Claude sessions see
it on load.

## What this does NOT change

- No \`.v\` files. The Coq code is untouched.
- No PR closures. PRs landed before this lockdown remain as-is.
- No deletion of \`PRESERVATION-HANDOFF.md\`; the per-case diagnostic
data may still inform layered-design work.

## Test plan

- [x] \`cat CLAUDE.md\` renders sensibly at repo root
- [x] \`PRESERVATION-DESIGN.md\` banner is the first visual block after
the title
- [x] \`ROADMAP.adoc\` no longer contains "Lemma B" / "5-phase" / "close
preservation to Qed" as instructions
- [x] No Coq files modified (no rebuild needed)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
…1 narrow admit (#178)

## Summary

Replaces the opaque `Axiom region_liveness_at_split_l1` with a
structurally-proved `Lemma … Admitted.` that closes **24 of 26 inductive
cases concretely**, leaving exactly 1 admit at the documented
counterexample sub-case (T_Region_Active_L1 with binder = rv).

The lemma's STATEMENT is unchanged — still universal `forall e`, still
false in the residual sub-case. **This PR is about transparency of proof
debt, not soundness.** The remaining admit accepts the same false
sub-case the Axiom did. But future closure work now has a clearly
identified target rather than an opaque hide-all.

## Closure pattern (24/26 cases proved concretely)

| Case class | Count | Discharge |
|---|---|---|
| R-unchanged base (T_Unit, T_Bool, T_I32, T_Var_*, T_Loc, T_StringNew,
T_Lam, T_Borrow, T_Borrow_Val) | 10 | `try assumption` (IH-free;
hypothesis [In rv R] = goal) |
| Compound (T_StringConcat, T_StringLen, T_Let, T_LetLin, T_App, T_Pair,
T_Fst, T_Snd, T_Inl, T_Inr, T_Drop, T_Copy) | 12 | IH chain |
| Branch-converging (T_Case, T_If) | 2 | IH through R1 to R_final |
| T_Region_L1 (fresh binder, ~In r R) | 1 |
`remove_first_L1_count_other` (r ≠ rv from ~In r R ∧ In rv R) |
| T_Region_Active_L1 r ≠ rv | 1 (sub-case) | same as T_Region_L1 |
| **T_Region_Active_L1 r = rv** | **1 (sub-case)** | **`admit.` —
GENUINELY FALSE** |

The remaining admit is at `formal/Semantics_L1.v:1055`. Documented
source-level counterexample:

```
ERegion rv (EI32 5) : TBase TI32 -| []  at  R = [rv]
```

The rule pops the only `rv` from `R_body`, so `In rv R = True` but `In
rv R' = False`.

## Closure paths forward (in-file + proof-debt.adoc)

- **(i)** Restate with a `no_region_active_pop_of rv e` side condition
and discharge at the 9 call sites in `subst_typing_gen_l1` (smallest
step, consistent with §4.8 closure approach (b)).
- **(ii)** Multi-set `region_env` (substantial L1 redesign).
- **(iii)** Weaker contextual signature.

(i) is the smallest step and the recommended next slice.

## Side update: `docs/proof-debt.adoc`

- Refreshed line numbers post-#170 + post-this-PR (entries now point to
actual current positions in `Semantics_L1.v`).
- Replaced the Axiom L903 entry with the Lemma L998 + admit L1055 +
Admitted L1068 trio.
- Echo.v K entry updated to note PR #173's K-freedom closure (no more
current escape hatch in Echo.v).

## Branch base

Stacked off `proof/l1-region-threading-design` (head `f03d7e7`,
post-#173).

## Test plan

- [x] `coqc 8.18.0` builds `Semantics_L1.v` cleanly
- [x] Clean full-project rebuild passes — 9 .v files including Echo.v,
Modality.v, TypingL2.v
- [x] `Counterexample.v` still Qed (regression test for the L1 design
counterexample)
- [x] 0 Axiom declarations in `Semantics_L1.v` (down from 1)
- [x] `Print Assumptions subst_preserves_typing_l1` still mentions
`region_liveness_at_split_l1` (now as an opaque Admitted-Lemma, not
Axiom — same logical state)
- [x] `proof-debt.adoc` line numbers cover all 9 current escape-hatch
positions (8 admits/Admitted + 1 Lemma-name marker)
- [ ] CI green on the next #153 cycle

## Caveats

- This is **not a soundness improvement**. The lemma's statement is
universal, the residual sub-case is genuinely false, and the `Admitted.`
makes Coq accept it the same way `Axiom` did.
- The improvement is **proof-debt visibility**: 24 cases now have
concrete witnesses, the residual obstacle has a clear narrow definition,
and closure work can attack just one specific structural sub-case.

Refs PR #153, PR #169, PR #170, PR #173, PRESERVATION-DESIGN.md §4.8 +
§4.8.1 + §5.1.

🤖 Generated with [Claude Code](https://claude.com/claude-code)
hyperpolymath added a commit that referenced this pull request May 27, 2026
…ation patching

The 2026-05-27 owner directive landed on the proof/l1-region-threading-design
branch (PR #175) but the L2 hybrid path (PRs #176 + #177) shipped
directly to main, leaving the lockdown stranded on a DIRTY+superseded
branch. This commit replays the directive to main where every future
session sees it.

Files updated:

- CLAUDE.md — APPENDS a new "🛑 Owner directive 2026-05-27" section
  to the existing disambiguation-focused file. TL;DR + DO/DO NOT list
  + anti-pattern detector + "if you're unsure" escalation policy +
  memory-store hooks. Preserves all existing disambiguation content.

- formal/PRESERVATION-DESIGN.md — adds 🛑 CANONICAL banner at top
  listing the four anti-patterns to refuse (close legacy preservation,
  extend Semantics.v for closure, ad-hoc-close Semantics_L1.v axioms,
  follow pre-discovery closure plans).

- formal/PRESERVATION-HANDOFF.md — strengthens banner from "🟠
  Superseded" to "🛑 ARCHAEOLOGY ONLY — do NOT follow the closure
  plans in this file." Names step_preserves_type_at_pre /
  step_output_context_eq_at_pre explicitly as in-class patching
  helpers.

- ROADMAP.adoc — preservation table row rewritten in layered terms
  (red status with "provably false, do not attempt to close").
  v0.1.0 checkbox rewritten as "re-derive preservation in the
  four-layer architecture" with status of L1/L2/L3/L4. The 250-line
  §"Preservation closure plan" body removed; replaced with a
  superseded-pointer section. Git history retains the original.

- .machine_readable/6a2/STATE.a2ml — next_action rewritten to layered
  framing. Adds a new @directive block (canonical=CLAUDE.md, source=
  owner, date=2026-05-27) so machine consumers see the same
  do/do-not list. last_action updated. @blockers + @artifacts
  reflect post-L2-hybrid main.

Other .machine_readable/* files audited (META, ECOSYSTEM, AGENTIC,
NEUROSYM, PLAYBOOK, ANCHOR, CLADE) — no stale patching references
found.

Companion memory entry:
~/.claude/.../memory/feedback_ephapax_no_patching_legacy_preservation.md

Closes the loop on issue #171 (strategic question) — the directive
is now visible on main to humans and machines.

PR #153 (proof/l1-region-threading-design) becomes safe to close as
superseded by the L2 hybrid path. Stranded contents:
  - my PR #170 (T_Var_*_L1 strengthening) — superseded; main's
    has_type_l1 has a different rule structure post-modality
    parameter, T_Var rules differ.
  - my PR #175 (lockdown) — replayed by this commit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
Brings three doc-only improvements from the design branch onto main:

1. PRESERVATION-DESIGN.md §4.8.1 (from design-branch PR #170 — T_Var
   strengthening landed via the m-indexed has_type_l1 in #176). Docs
   what §4.8 path (3) closes and what it does not.

2. PRESERVATION-DESIGN.md §5.1 (from design-branch PR #172) —
   L1's lambda-rigidity gap (S_App_Step2 / S_Pair_Step2 admits in
   preservation_l1) closes at L2 Phase 2 via effect-typed TFun.
   Documents the §5 table's "✓ (L1 fix)" cell as conditional, and
   explains why effect-typing is L2's job not L1's.

3. docs/proof-debt.adoc — adds the L1 admit enumeration that the
   design branch carried via PR #169. Eight current escape-hatch
   sites in Semantics_L1.v listed by file:line per the
   trusted-base policy substring-match convention. Plus the Echo.v
   K-closure note (from PR #173's main re-port).

No source/proof changes — pure documentation. Allows the
trusted-base reduction policy check to substring-match all
escape-hatch sites in Semantics_L1.v.

Refs design-branch PRs #169 / #170 / #172 / #173, PR #176 (L2 hybrid).
hyperpolymath added a commit that referenced this pull request May 27, 2026
## Summary

Brings three doc-only improvements from the (now-superseded) design
branch onto main. All are pure documentation; no source/proof changes.

## What this PR adds

### 1. `PRESERVATION-DESIGN.md` §4.8.1 (from design-branch PR #170)

Records that path (3) — `T_Var_*_L1` strengthening — landed via the
m-indexed `has_type_l1` in #176. Documents what it closes (source-level
variable soundness gap) and what it does not (the lambda-rigidity gap in
`S_App_Step2` / `S_Pair_Step2`).

### 2. `PRESERVATION-DESIGN.md` §5.1 (from design-branch PR #172)

L1's lambda-rigidity gap closes at **L2 Phase 2** via effect-typed
`TFun`, not at L1. Documents:
- The §5 table's "✓ (L1 fix)" cell flagged with `(*conditional on
§5.1*)`.
- Why path (3) (T_Var strengthening) is necessary-not-sufficient.
- Proposed effect-typed `TFun` signature: `TFun T1 T2 (R_in :
region_env) (R_out : region_env)`.
- Why effect-typing is L2's job (typing-layer concern, not
region-layer).
- Sequencing: L2 Phase 2 follow-up to current `T_Lam_L1_*` rules.

### 3. `docs/proof-debt.adoc` — L1 admit enumeration (from design-branch
PR #169)

Adds the eight current escape-hatch sites in `Semantics_L1.v` listed by
`file:line` per the standards#203 trusted-base policy substring-match
convention:

- L343, L400, L412, L520 (region-shrink admits)
- L608 (Axiom `region_liveness_at_split_l1`)
- L632 (preservation_l1 Admitted)
- L703 / L704 (lambda-rigidity admit + Admitted)

Plus the Echo.v K-closure note (from PR #173's main re-port).

## Why this matters

Three independent improvements that the parallel-session #176 bundling
didn't include. Each is small enough to ship as part of a single docs
cleanup:

- **§4.8.1**: makes the §4.8 status accurate post-#170/#176 landing.
- **§5.1**: makes the §5 table honest about the lambda-rigidity gap.
- **proof-debt.adoc**: enables `trusted-base reduction policy` check to
substring-match all current L1 escape-hatch sites by file:line.

## Companion PRs

- **#180** — K-free Echo.v rewrite (port of design-branch #173). No
conflict with this PR.
- **#181** — Axiom→Lemma conversion for `region_liveness_at_split_l1`
(port of #178, adapted to m-indexed `has_type_l1`). When #181 lands, the
L608 `Axiom` entry in this PR's proof-debt.adoc will become stale —
follow-up doc tweak to update the line numbers post-#181.

## Test plan

- [x] Asciidoc / Markdown lints (renders in GitHub preview)
- [x] All eight current L1 escape-hatch sites covered by `file:line`
substring matches
- [x] §4.8.1 + §5.1 wording matches the design-branch versions
- [ ] CI green (the doc changes shouldn't trigger any Coq build steps)

Refs design-branch PRs #169 / #170 / #172 / #173, PR #176 (L2 hybrid),
PRs #180 and #181 (companion).

🤖 Generated with [Claude Code](https://claude.com/claude-code)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant