Exitify.v: 3 Admitted, regression from GHC 9.10 type changes

[lastland]

Context

The Exitify module verifies that GHC's exitifyRec transformation preserves well-scopedness and join point validity — a key result from "Embracing a Mechanized Formalization Gap" (arxiv:1910.11724).

History

• Before PR Migrate hs-to-coq to GHC 9.10.3 and Coq 8.20 #209 (ghc8-coq810): exitifyRec was a concrete Definition in lib/Exitify.v (0 Axioms in lib), and all proofs in theories/Exitify.v were complete — 0 Admitted. The deferredFix_eq_on proof idiom successfully extracted local definitions and proved go_eq.
• PR Migrate hs-to-coq to GHC 9.10.3 and Coq 8.20 #209 (GHC 9.10): exitifyRec remains a concrete Definition in lib/Exitify.v (not axiomatized). However, GHC 9.10 changed Core types significantly (Alt uses Mk_Alt constructor instead of tuple, Mk_Id has 7 fields with varMult : Mult added 4th, Var has single Mk_Id constructor). These type changes broke the existing deferredFix2 proofs in theories/Exitify.v. The main paper theorem exitifyProgram_WellScoped_JPV was re-proved (Admitted → Qed), but three sub-lemmas remain Admitted. Additionally, mkExitJoinId is a new Axiom in lib/Exitify.v (needs Mult/ManyTy type not in translation).
• Classification: Regression in theories (0→3 Admitted). The proofs worked before and can likely be restored by porting the proof scripts to GHC 9.10 types.

Current State

3 Admitted in examples/ghc/theories/Exitify.v:

Lemma	Line	Description
exitifyRec_WellScoped	339	exitifyRec preserves WellScoped
exitifyRec_JPI	347	exitifyRec preserves join point validity
top_go_WellScoped_JPI	467	top-level go preserves both invariants

The first two require extracting local definitions from exitifyRec via cbv beta delta + proving go_eq using deferredFix_eq_on with the GoDom predicate (~1500 lines). The third requires ~200 lines of Program Fixpoint structural induction on CoreLT.

Impact

The main paper theorem exitifyProgram_WellScoped_JPV is Qed but composes these 3 Admitted lemmas via exitifyRec_WellScoped_JPI. If any sub-lemma is false, the composed theorem is unsound.

Potential Solutions

1. Port the pre-GHC 9.10 deferredFix2 proofs (from ghc8-coq810 tag) to the new Core types. The proof pattern is known to work — it's a matter of updating for Mk_Alt, 7-field Mk_Id, etc.
2. Simplify by extracting go as a standalone Program Fixpoint.

Acceptance Criteria

• All 3 lemmas proved (Qed)
• 0 Admitted in Exitify.v

---

This issue was generated with the help of Claude Code. @lastland has checked these issues before posting.