docs: SUBST-LEMMA-GENERALIZATION-DESIGN — Phase D slice 4 plan#213
Merged
hyperpolymath merged 1 commit intoMay 28, 2026
Merged
Conversation
…mma generalisation plan Captures the architectural analysis identified by PR #211: full preservation_l2 over has_type_l2 blocks at T_App_L2_Eff β-case on subst_typing_gen_l1_m's is_linear_ty T1 = true precondition. Generalising to non-linear T1 is more complex than a "sibling lemma with false instead of true" — it interacts with body-R- rigidity for non-linear ELam values. Doc contents: - Why this matters (T_App_L2_Eff β-case structural obligation) - Two distinct uses of Hlin in the existing proof: (A) linear_value_is_loc_l1 canonical-form extraction (B) T_Var_Unr_L1 contradiction discharge - Body-R-rigidity issue: fully general nonlinear_value_retype is FALSE for TFun lambdas (legacy slice 4b debt) - Per-value-shape retype-feasibility table (ground / TFunEff / TFun / pair / sum / borrow / echo) - Recommended 5-phase approach: Phase 1: ground_nonlinear_retype_l1_m (10-line lemma) Phase 2: subst_typing_gen_l1_m_ground_nonlinear (~250 lines) Phase 3: tfuneff_lambda_retype + extended subst (for higher- order beta) Phase 4: close preservation_l2 β-case Phase 5 (deferred): compound non-linear values - Owner-directive compliance check (passes all anti-pattern detectors) - 4 open design questions for owner What this session ships: - This design document only. No code changes. Next session (per STATE.a2ml shift in companion PR): - Phase 1: implement ground_nonlinear_retype_l1_m in formal/Semantics_L1.v Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 73 issues detected
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
added a commit
that referenced
this pull request
May 28, 2026
) ## Summary Reflect the deeper analysis from PR #213's design doc: the non-linear substitution generalisation is a **5-phase plan, not a single sibling lemma**. Phase 1 (the simplest ~10-line building block) is the right next-session scope. ## Changes - **\`next_action\`**: shift from "generalise subst_typing_gen_l1_m (full scope)" → "Phase 1: \`ground_nonlinear_retype_l1_m\`". Cites the design doc + identifies the two file touchpoints (\`Syntax.v\` predicate, \`Semantics_L1.v\` lemma). - **\`last_action\`**: record PR #213 design doc merge. - **\`@artifacts\`**: extend to list \`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md\`. Anti-pattern list updated to include design-doc-specific guardrails: no folding case-split into existing lemma, no closing TFun retype (legacy slice 4b gap, out of scope), etc. ## Refs - PR #213 — design doc (merged) - PR #211 — preservation_l2_via_l1 (merged) - \`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md\` 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Merged
5 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…r TBase TUnit/TBool/TI32 (#219) ## Summary Phase 1 of the non-linear substitution-lemma generalisation per [`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`](https://github.com/hyperpolymath/ephapax/blob/main/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md) §"Phase 1" (design doc landed in #213). Adds NEW infrastructure to L1, **orthogonal to legacy preservation** in `Semantics.v` (that theorem remains correctly `Admitted` — provably false per `Counterexample.v`, per owner directive 2026-05-27): - `is_ground_nonlinear_ty : ty -> bool` in `formal/Syntax.v` (after `is_linear_ty`). - `ground_nonlinear_retype_l1_m` in `formal/Semantics_L1.v` (after `loc_retype_at_R_l1_m`): ```coq forall m R R' G v T, is_value v -> is_ground_nonlinear_ty T = true -> has_type_l1 m R G v T R G -> has_type_l1 m R' G v T R' G. ``` Proof destructs on the `is_value v` witness; EUnit/EBool/EI32 cases invert + re-apply the corresponding R-polymorphic ground constructor at R'; non-ground value cases (ELam/EPair/EInl/EInr/ELoc/EBorrow/EEcho) discriminate `Hgrd` against the non-ground codomain type every typing-rule inversion produces. ## Why this matters The `T_App_L2_Eff` β-case of `preservation_l2` is blocked at non-linear `T1` (in `TFunEff T1 T2 R_in R_out` lambdas) because `subst_typing_gen_l1_m`'s `is_linear_ty T1 = true` precondition can't fire for non-linear ground types (`TBase TUnit` / `TBase TBool` / `TBase TI32`). Phase 1 ships the ground-non-linear retype primitive that Phase 2's parallel substitution lemma will use in place of `loc_retype_at_R_l1_m` for R-shift retypes. ## Owner-directive compliance Per `CLAUDE.md` 2026-05-27 (escalated again in #213 design doc §"Owner-directive compliance check"): - Does NOT close `Theorem preservation` in `Semantics.v`. - Does NOT extend `Semantics.v` / `Typing.v` / `Counterexample.v` (all untouched in diff). - Does NOT close residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. - Adds no new `Axiom` or `Admitted` declarations. - Follows post-2026-05-26 four-layer redesign per `PRESERVATION-DESIGN.md`. ## Test plan - [x] `just clean && just all` in `formal/` — clean rebuild of all 10 `.v` files (coqc 8.18.0). - [x] Zero new admits/axioms (proof is `Qed`). - [x] `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. - [x] GPG-signed commit. - [x] STATE.a2ml `next_action` shifted to Phase 2 design. ## Refs Refs hyperpolymath/standards#134 (sub-issue of hyperpolymath/standards#124 estate proof-debt epic). Follows #213 (design doc). Phase 2 (parallel substitution lemma) is the next slice. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…is_tfuneff_ty` (#224) ## Summary - Ships the **retype lemma half** of Phase 3 per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`. - Adds `is_tfuneff_ty` predicate (Syntax.v) mirroring `is_ground_nonlinear_ty`. - Adds `tfuneff_lambda_retype_l1_m` lemma (Semantics_L1.v): retype TFunEff lambda value across `(m, R, G) → (m, R', G)` under side condition `forall r, In r R' → In r R_in`. - **Phase 3b (substitution-lemma extension) DESCOPED** to a follow-up PR after structural analysis revealed the `T_Region_L1` fresh-region obstacle. STATE.a2ml documents the three candidate solutions. ## Why split `SUBST-LEMMA-GENERALIZATION-DESIGN.md` Phase 3 proposed two pieces (retype + substitution extension). Walking the substitution proof revealed: every retype across a threaded `R_n` inside the term `e` demands `forall r, In r R_n → In r R_in_arg`, and `T_Region_L1` firings inside `e` introduce fresh `r ∉ R_outer` — freshness wrt the threaded R does **not** imply membership in the value-type's fixed `R_in_arg`. Three candidate fixes (syntactic side condition on `e`; universal-R Hv_type with per-case discharge; restrict to region-free terms) need Phase 4 prototyping of the actual `subst 0 varg ebody` shape before choosing. Phase 3a's retype lemma stands on its own as clean infrastructure usable in 3b and Phase 4. ## Proof shape `tfuneff_lambda_retype_l1_m`: - `destruct Hval` (10 value-form cases) - `inversion Ht; subst; try discriminate` - Non-ELam forms: types don't match TFunEff → `discriminate`. - ELam at TFun (legacy rules `T_Lam_L1_Linear` / `T_Lam_L1_Affine`): type mismatch TFun ≠ TFunEff → `discriminate`. - ELam at TFunEff (`T_Lam_L1_Linear_Eff` / `T_Lam_L1_Affine_Eff`): re-apply rule with new `Hsub`, body via `eassumption`. Zero new admits, zero new axioms. Coqc 8.18.0 clean rebuild across all 10 .v files. ## Owner-directive compliance (per `CLAUDE.md` 2026-05-27) - ✅ No closure of legacy `preservation` in `Semantics.v` (untouched). - ✅ No closure-support lemmas in `Semantics.v` (untouched). - ✅ No closure of residual `Semantics_L1.v` admits — strictly NEW orthogonal infrastructure. - ✅ No patching `Typing.v` (untouched). - ✅ No new `Admitted` / `Axiom`. - ✅ Anti-pattern detector clean. ## Test plan - [x] `coqc -Q . Ephapax` clean across all 10 .v files locally. - [ ] CI green on `formal/` build job. Refs: standards#134 (proof-debt epic), #220 (Phase 2), #213 (design doc).
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
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.
Summary
Design document capturing the architectural analysis from PR #211: full `preservation_l2` over `has_type_l2` blocks at the T_App_L2_Eff β-case on `subst_typing_gen_l1_m`'s `is_linear_ty T1 = true` precondition. Generalising to non-linear `T1` is more complex than a "sibling lemma with `false` instead of `true`" — it interacts with body-R-rigidity for non-linear `ELam` values (the same gap that blocks legacy `preservation_l1` slice 4b).
What this PR ships
Key findings documented
Two distinct uses of `Hlin` in the existing proof:
Body-R-rigidity issue: a fully general `nonlinear_value_retype_at_R_l1_m` lemma is FALSE for TFun lambdas — the legacy slice 4b debt re-surfaces at the retype layer. TFunEff lambdas escape this trap via their `R_in ⊇ R` side condition.
Per-value-shape feasibility table (in doc): ground non-linear ✅ trivial; TFunEff⚠️ tractable; TFun ❌ blocked; compound ⚠️ inherits.
Recommended 5-phase plan
Open design questions for owner (in doc)
Owner-directive compliance
Checked in §"Owner-directive compliance check" of the doc. Passes all anti-pattern detectors.
Refs
Test plan
🤖 Generated with Claude Code