Skip to content

proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit#181

Merged
hyperpolymath merged 1 commit into
mainfrom
proof/l1g-axiom-lemma-on-main
May 27, 2026
Merged

proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit#181
hyperpolymath merged 1 commit into
mainfrom
proof/l1g-axiom-lemma-on-main

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Adaptation of design-branch PR #178 to main's m-indexed has_type_l1 (per #176). Replaces the opaque universal Axiom region_liveness_at_split_l1 with a structurally-proved Lemma … Admitted. that closes 28 of 29 inductive cases concretely, leaving exactly 1 admit at the documented counterexample sub-case (T_Region_Active_L1 with binder = rv).

Structure

  1. region_liveness_at_split_l1_gen — generalised over the modality parameter m. Induction handles all 29 constructors including the mode-split T_Lam_L1_Linear/Affine, T_Case_L1_Linear/Affine, T_If_L1_Linear/Affine.

    • R-unchanged cases (11) auto-discharge via try assumption.
    • Compound cases (16) route IH chains.
    • T_Region_L1 (fresh binder) closes via remove_first_L1_count_other (~In r R ∧ In rv R gives r ≠ rv).
    • T_Region_Active_L1 splits on r =? rv:
      • r ≠ rv: same remove_first_L1_count_other argument.
      • r = rv: GENUINELY FALSE — admit with documented counterexample.
  2. region_liveness_at_split_l1 — Linear-specialised wrapper matching the original Axiom's signature for existing call sites in subst_typing_gen_l1. One-line proof by eapply on _gen.

What this is and isn't

Is: a proof-debt transparency improvement. 28 cases now have concrete witnesses; the residual obstacle is one narrowly-defined sub-case with a source-level counterexample.

Isn't: a soundness improvement. The lemma's statement is universal forall e, still false in the residual sub-case, still accepted by Admitted. the same way Axiom was. Counterexample:

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

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

Closure paths forward (in-file)

  • (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).
  • (ii) Multi-set region_env (substantial L1 redesign).
  • (iii) Weaker contextual signature.

Verification

  • 0 Axiom declarations in formal/Semantics_L1.v (down from 1)
  • Full project rebuild: 9 .v files clean
  • Counterexample.v still Qed (regression test for the L1 design counterexample)
  • Print Assumptions subst_preserves_typing_l1 still mentions region_liveness_at_split_l1 (now as opaque Admitted-Lemma, not Axiom — same logical state)

Test plan

  • coqc 8.18.0 builds cleanly
  • Clean full-project rebuild passes — 9 .v files
  • 0 Axiom declarations in Semantics_L1.v
  • CI green

Refs PR #178 (design-branch original), PR #176 (L2 hybrid + m-indexing).

🤖 Generated with Claude Code

…1 narrow admit

Adaptation of design-branch PR #178 to main's m-indexed has_type_l1
(per #176). Replaces the opaque universal Axiom with a structurally-
proved Lemma that closes 28 of 29 inductive cases concretely, leaving
exactly 1 admit at the documented counterexample sub-case
(T_Region_Active_L1 with binder = rv).

Structure:

- region_liveness_at_split_l1_gen — generalised over the modality
  parameter m. Induction handles all 29 constructors including the
  mode-split T_Lam_L1_Linear/Affine, T_Case_L1_Linear/Affine,
  T_If_L1_Linear/Affine. R-unchanged cases auto-discharge via
  [try assumption]; compound cases route IH chains; T_Region_L1
  (fresh) closes via [remove_first_L1_count_other]; T_Region_Active_L1
  splits on r =? rv with the false sub-case admitted.

- region_liveness_at_split_l1 — Linear-specialised wrapper matching
  the original Axiom's signature for existing call sites in
  subst_typing_gen_l1. One-line proof by eapply on _gen.

The lemma's STATEMENT is unchanged (still universal forall e, still
false in the residual sub-case at T_Region_Active_L1 r=rv). The
Admitted accepts the same false sub-case the Axiom did. This is a
proof-debt TRANSPARENCY improvement, not a soundness improvement.

Counterexample at the source level (typed at R = [rv]):

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

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

Closure paths forward (in-file comment):
  (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.

Verification:
- 0 Axiom declarations in formal/Semantics_L1.v (down from 1)
- Full project rebuild: 9 .v files clean
- Counterexample.v still Qed (regression test)
- Print Assumptions on subst_preserves_typing_l1 still mentions
  region_liveness_at_split_l1 (now as an opaque Admitted-Lemma,
  not Axiom — same logical state)

Refs PR #178 (design-branch original), PR #176 (L2 hybrid +
m-indexing), PR #153 (superseded design branch).
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 38 issues detected

Severity Count
🔴 Critical 9
🟠 High 10
🟡 Medium 19

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (14 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (11 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (5 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Admitted leaves proof hole (3 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (7 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit a54ecb7 into main May 27, 2026
17 checks passed
@hyperpolymath hyperpolymath deleted the proof/l1g-axiom-lemma-on-main branch May 27, 2026 11:57
hyperpolymath added a commit that referenced this pull request May 27, 2026
…t pointer

The CORE INVARIANTS section in 0-AI-MANIFEST.a2ml claimed "All proofs
MUST remain closed (67/67 Qed)" — false as of mid-2026:

- formal/Semantics.v `preservation` is Admitted (provably FALSE per
  Counterexample.v's 3 Qed lemmas).
- formal/Semantics_L1.v carries 4+ admits + 1 Admitted Lemma
  region_liveness_at_split_l1_gen (post-#181) + 1 Admitted
  preservation_l1.

The trusted-base reduction policy (standards#203) is the canonical
enforcement mechanism — every escape hatch is enumerated by
file:line in docs/proof-debt.adoc. Replace the 67/67 number with a
pointer to that mechanism, and strengthen the rule: ANY new escape
hatch must be enumerated in docs/proof-debt.adoc before the
trusted-base CI check will pass.

Refs PR #176 (L2 hybrid), PR #181 (Axiom→Lemma), PR #164 (proof-debt
seed), standards#203.
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)
hyperpolymath added a commit that referenced this pull request May 27, 2026
…t pointer (#183)

## Summary

`0-AI-MANIFEST.a2ml`'s CORE INVARIANTS section claimed "All proofs MUST
remain closed (67/67 Qed)" — false as of mid-2026. Replaces with an
honest pointer to the trusted-base reduction policy.

## Why it was wrong

- `formal/Semantics.v` `preservation` is `Admitted` (and provably FALSE
per `Counterexample.v`'s 3 Qed lemmas).
- `formal/Semantics_L1.v` carries 4+ admits + 1 Admitted Lemma
`region_liveness_at_split_l1_gen` (post-#181) + 1 Admitted
`preservation_l1`.

The "67/67" number doesn't match either pre-L1-redesign or post-redesign
reality.

## What replaces it

A pointer to the canonical enforcement mechanism —
`docs/proof-debt.adoc` (per standards#203) — which substring-matches
every escape hatch by `file:line`. Plus a strengthened rule: ANY new
escape hatch must be enumerated in `docs/proof-debt.adoc` before the
trusted-base CI check will pass.

## Diff

1 line changed.

## Test plan

- [x] Renders correctly
- [ ] CI green (docs-only change)

Refs PR #176 (L2 hybrid), PR #181 (Axiom→Lemma), PR #164 (proof-debt
seed), standards#203.

🤖 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