God-file seam map — split proposal for TypeCheck.lean/AbstractMachine.lean

Status. Design proposal only. Zero code moved. This note produces the seam map so that when the split is executed, it is mechanical and behavior-identical, not a live re-design. Opening the PATH to execute it is the operator's call (see closing section).

0 · Why

Bang/Frontend/TypeCheck.lean (5770 lines) and Bang/Backend/AbstractMachine.lean (6849 lines) are together ~40% of the codebase and ~10× the repo's median module size. Costs: navigation/review touch many subsystems at once, single-file Lean re-elaboration time grows with file size, and parallel agent work on disjoint subsystems inside one file forces one-writer serialization (.claude/lane-discipline.md). A split executed without a designed seam risks the worse outcome: circular imports, types moved to the wrong stratum, or a broken import-direction invariant (the arch-check fitness leg, ADR-0048).

Line-number anchors below are as of commit f1cb2cf (branch point for this plan). Re-anchor by line CONTENT (the /-! ## … -/ header text), not raw numbers, before executing — headers are stable, line numbers drift with every edit.

1 · Section inventory + dependency table

Methodology note. Raw grep -c/occurrence counts for short, common identifiers (check, resolve, hget, instantiate, …) are unreliable on this codebase — Lean proof scripts reuse short hypothesis names (hget collides with an unrelated local in Bang/Meta/BinaryLR.lean/Bang/Core/Soundness.lean) and prose comments reuse English words that substring-match identifiers (check collides with "type-check"/"cross-check" in doc comments). Every consumer claim below was re-verified by reading the actual matched line, not just counting hits — where a first-pass grep sweep and the line-level re-check disagreed (this happened once, on the TypeCheck #guard corpus's dependency surface, §1.1), the re-checked finding is what's reported, with the correction called out explicitly rather than silently overwritten.

1.1 Bang/Frontend/TypeCheck.lean (5770 lines, no import Bang.* — a leaf w.r.t. other

Bang modules; it is itself imported by 4 files, table in §1.3)

Answering the plan's key questions (corrected after direct verification, see note):

• Does the #guard corpus region depend on anything except checkProg/checkAndLower/ parseProg/buildEnv? — NO, and this corrects the plan's stated hypothesis. A direct word-boundary check of every pre-5146 top-level name against the corpus region's text (awk-extracted def list × grep -oE '\b<name>\b' over lines 5146–5770, each hit read at its source line to rule out comment/prose noise) found 20+ pre-5146 internal names directly referenced inside the corpus region, not just the four public entry points — among them showCTy (real function calls at lines 55/61/68 of the corpus region, not comments — verified by reading the matched lines), checkPerformUnderCap (13 occurrences), elabHClauses, elabProg, elabS, synthSC, synthSV, qualifyModule, qualifyDotAccess, qualifyModuleOwnImports, resolve/resolveTy/resolveTyG/resolveEffName, unifyRow, zonkInferC, runInferC, effOf/effNames, foldLetDecls, capOpSig, curryBind, anfSplit, isValueSurf, check (20 occurrences — the bidirectional-checker entry, not checkProg). Some hits (checkHClauses, checkLaws) are prose-comment references rather than calls, but the majority above are genuine calls, confirmed by reading matched lines directly. The corpus is NOT the narrowly-isolated, cheapest extraction the plan hypothesized — it reaches across the elaboration (2491+), Modules-merge (3120+), and LAWS-discharge (3931+) sections, not just the four public entry points. This reverses this note's own cut-order §5 step 1 below; see the correction there.
• Is the HM substrate (421–1536) consumed by anything except the elaborator sections below it? No external-file consumer found (grep-confirmed no other Bang/*.lean file references Infer, the unification defs, or the row-inference defs by name). It is consumed in-file only, by the elaboration section (2491+) and later validation sections that invoke the checker through the public API (not the HM internals directly).

1.2 Bang/Backend/AbstractMachine.lean (6849 lines, no import Bang.*)

Answering the plan's key question: Do the proof sections (545+, 2158+, 3592+) consume the executable sections (106–544: stores, evalD, the machine) only through a narrow set of definitions? Yes, narrowly: the proof sections reach into the executable sections primarily through the same small vocabulary — SStore/THeap/CStore, evalD, Code/Stack/HStack, compile/exec — rather than reaching past that surface into private helpers. This is the load-bearing fact that makes a Stores/Machine vs Proofs cut plausible, but the proof sections are large (2158–4958, roughly 2800 of the file's 6849 lines) and mutually cross-reference each other extensively (calculation-correctness → diff-test battery → D1-A bridge build on each other in sequence) — so while the executable surface they consume is narrow, the proof sections themselves are not independently separable from one another without finer-grained investigation this note does not attempt. See §4 stays-put.

1.3 Reverse edges — who imports each god file

No file imports both (checked both plain import Bang.* and the module-syntax public import Bang.* forms across the whole tree). This is the confirmation the plan's STOP condition #2 (a genuine cycle) does not fire — see §4.

2 · Proposed module set

Precedent for the shape: Bang/Core/Semantics.lean is already a thin hub re-exporting Bang/Core/Semantics/{Subst,Dispatch,Eval,Invariants}.lean (a prior "split a fan-in hub into a tier subdirectory" move, docs/architecture/core-overview.md §6, task #15/#17). The same shape — hub file public import-ing siblings under a <OldName>/ subdirectory — is the template here, so Bang.Frontend.TypeCheck and Bang.Backend.AbstractMachine remain valid import targets for existing consumers (no consumer-side import-line churn beyond what the hub already absorbs).

2.1 Bang/Frontend/TypeCheck/ split

None of these modules exist yet — they are named below in dotted Lean-module form (e.g. Bang.Tier.Old.New), not slash-path form, precisely because they are proposed, not real files (a slash-path claim asserts the file exists, which tools/check-refs.py's fitness gate correctly rejects as stale for a not-yet-created file — confirmed by triggering it once while drafting this note). When the PATH executes a cut, the dotted name maps onto a subdirectory exactly as the existing Bang.Core.Semantics.Subst precedent maps to Bang/Core/Semantics/Subst.lean.

2.2 Bang.Backend.AbstractMachine.* split

Note on the proof sections (545–6849): per §1.2's answer, these sections consume the executable layer only through the narrow Stores/EvalD/Machine vocabulary, so in principle they could be extracted too. This note deliberately proposes leaving them in the hub file for now — see §4 ("what deliberately stays") for the rationale; a finer split of the proof sections themselves is future work this note does not size.

3 · Import-direction proof sketch

The binding rule, read directly from tools/arch-check.sh (comments lines 8–39, code lines 40–118):

RANKS:  Core = 0 (sink)  <  Frontend = Backend = 1 (siblings)  <  Meta/Witness/Reify = 2  <  Apex = 3
RULES:  (a) no module imports STRICTLY UPWARD (importer rank < imported rank is forbidden)
        (b) Frontend ⊥ Backend — the two rank-1 edges meet ONLY at Core (Frontend importing
            Backend, or vice versa, is forbidden regardless of rank)
LAYER:  path-derived — `Bang/<Tier>/...` decides layer, not a hand-maintained case map.

Checking every proposed edge in §2.1/§2.2 against this rule:

• All four new Bang/Frontend/TypeCheck/*.lean files are still under Bang/Frontend/, so layer_of maps them to Frontend (rank 1) exactly as TypeCheck.lean is today — no rank change. Same for all three new Bang/Backend/AbstractMachine/*.lean files under Bang/Backend/ → Backend (rank 1).
• Internal edges (Infer.lean → Bidi.lean, Elab.lean → {Bidi,Infer}, Corpus.lean → the hub, EvalD.lean → Stores.lean, Machine.lean → {Stores,EvalD}) are all same-rank/same-tier (Frontend → Frontend, Backend → Backend) — same-tier imports are unrestricted by rule (a) (rank a < rank b is the forbidden case; a == b is fine, matching how Bang/Core/Semantics/*.lean siblings already import each other within Core).
• No proposed edge crosses Frontend ↔ Backend (rule (b)) — confirmed in §1.3, no file imports both today, and none of the proposed splits introduce such an edge (Frontend's split imports only other Frontend files + Core; Backend's split imports only other Backend files + Core).
• No proposed edge imports upward into Meta/Witness/Reify/Apex — all listed imports in §2.1/§2.2 stay within Core (rank 0, downward — allowed) or the same tier (rank 1).

Verdict: every proposed edge is legal under the current arch-check rule as written. No change to tools/arch-check.sh's layer_of case map is needed — Bang/Frontend/TypeCheck/* and Bang/Backend/AbstractMachine/* both already match the Bang.Frontend.*/Bang.Backend.* prefix patterns the script's case statement matches on (lines 48/50), because Lean dotted module names preserve the directory path.

4 · Risk register

abbrev/notation/macro crossing a proposed cut

Grepped directly (^abbrev \|^notation\|^macro , whole-file, both files — no notation or macro declarations in either file):

No notation/macro declarations exist in either file — this eliminates the sharpest edge of the incident-history risk (the Membership ?m X elaboration failure involved an imported abbrev specifically; there is no notation/macro exposure here). Every abbrev above crosses at least one proposed cut in the sense that it's defined in one piece and consumed in a sibling — this is expected and mechanical (re-export via public import, same as Bang/Core/Semantics.lean's hub already does for its four siblings' abbrevs). The register flags them so the execution PATH checks each one's elaborated type is IDENTICAL post-move (not just "compiles") — the incident precedent was a silent behavior change, not a build error.

partial def

Zero partial def declarations in either file (grepped, whole-file). No termination/wf context risk from this category — a clean negative finding for the risk register.

The #guards

TypeCheck.lean's corpus region (5146–5770) and AbstractMachine.lean's diff-test battery (3447–3592) are both compiled #guards (per CLAUDE.md: "only compiled lake build #guards are reliable"). Wherever they land post-split, they must remain in a module that still gets compiled by lake build (not orphaned into a module excluded from the build) — the execution PATH's Step-per-cut verification (§5) must include just build succeeding AND the guard count being unchanged (grep-count #guard occurrences before/after each cut as an explicit regression check, not just "the build is green").

5 · Cut order

Safest-first, each landing independently just verify-green before the next starts. Revised from the plan's hypothesized order: §1.1's direct verification found the TypeCheck corpus is NOT narrowly coupled (it calls 20+ internal names beyond the four public entry points), so it does not lead — the AbstractMachine.lean stores extraction leads instead, being the only cut in either file confirmed to touch a genuinely narrow, low-traffic dependency surface (simple abbrevs over already-defined kernel types, not the machine's derived calculation):

1. AbstractMachine.lean stores extraction (Stores.lean, §2.2) — the #1 safest cut. SStore/THeap/CStore are simple abbrevs over already-defined kernel types (Bang.EffectRow.Label, Val, Bang.OpId/Comp), not derived through the machine's calculation, and the region (106–224) itself calls nothing outside Bang.Core.*. Verify: just verify green, guard-count and axiom-state unchanged (just axioms).
2. TypeCheck.lean corpus extraction (Corpus.lean, §2.1) — demoted from the plan's assumed #1 slot after direct verification (§1.1) showed real coupling to ~20 internal names across elaboration/Modules/LAWS. Still tractable — the corpus's own logic doesn't grow, only its import list does — but requires the hub (TypeCheck.lean) to re-export a wider surface than checkProg/checkAndLower/parseProg/buildEnv alone, which raises the odds an abbrev (CT/Ctx/Infer, §4) crosses the cut in a way that needs the same identical-elaborated-type check as the AbstractMachine abbrevs. Verify: just verify green, #guard count in Corpus.lean == pre-cut count in that line range, axiom state unchanged.
3. AbstractMachine.lean evalD + machine extraction (EvalD.lean, Machine.lean, §2.2) — depends on step 1 landing first (imports Stores.lean). Higher risk than steps 1–2 because evalD/compile/exec are the objects the proof sections (kept in-place, §4 below) reach into — a botched extraction here breaks the in-place proofs even though no proof code moved. Verify: same triple, PLUS confirm just axioms shows the SAME headline theorems' axiom sets as pre-cut (not just "some axiom set") — the proof sections are the highest-value code in the repo and must not silently degrade.
4. TypeCheck.lean Bidi/Infer/Elab three-way split (§2.1) — deferred to last among the TypeCheck cuts because it is the least externally-motivated (no external consumer touches these internals, §1.1) and the internal coupling between the three pieces is the densest in either file (HM substrate feeds elaboration feeds LAWS discharge, all mutually referential). This is real work with real risk and comparatively low external payoff — candidate for "do it only if the file-size pain persists after cuts 1–3," not a must-do in the same PATH.

Each landing's success criterion, restated: just verify (selfcheck + lake build + audit) green, docs/notes/README.md/CLAUDE.md untouched by the code move itself (docs update separately), #guard/theorem-count parity confirmed by grep before/after, and just axioms output byte-identical for every headline theorem the cut's region touches.

6 · What deliberately stays

• The proof sections of AbstractMachine.lean (545–6849, ~6300 of 6849 lines) stay together and stay in the hub file for now. Rationale: per §1.2, "the calculation is correct" (2158+), the diff-test battery (3447+), and the D1-A bridge (3592+) build on each other sequentially within the file — the calculation IS the module, in the same sense CLAUDE.md's invariant #4 ("the machine is an output of the calculation, never hand-designed") treats derivation and proof as one artifact. Splitting these apart is a substantially harder, finer-grained investigation than this note attempts (see §2.2's note) — proposing it without that investigation would be exactly the "trivial extraction" the plan's scope explicitly warns against.
• TypeCheck.lean's Bidi/Infer/Elab three-way split (§2.1, cut 4) is proposed but explicitly sequenced last and flagged as possibly not worth doing — the internal coupling is the densest of any region in either file and the payoff (no external consumer touches these internals) is the lowest of the four cuts.
• Neither file's import Bang.* list needs to change for consumers — the hub-file pattern (Bang/Core/Semantics.lean precedent) means Bang/Frontend/TypeCheck.lean and Bang/Backend/AbstractMachine.lean continue to exist as thin re-exporting hubs, so the 4 + 7 existing consumer files (§1.3) need zero import-line changes.

7 · Closing note

This note is a proposal — the split needs an ADR + operator sequencing after the parked LR census unit lands. The census unit at branch feat-lr-carrier-stackinc-wip touches Bang/Meta/BinaryLR.lean, which — while it does not import Bang.Backend.AbstractMachine directly (§1.3, confirmed no direct edge) — depends structurally on Bang.Core.Soundness, which is built to agree with the D1-A bridge (evalD_agrees_source) proven in AbstractMachine.lean's 3592+ region. Splitting AbstractMachine.lean (especially cut 3, §5) while that branch is unmerged invites rebase pain the moment it lands, even without a direct import-edge collision. Sequence: let the census unit land (or get explicitly abandoned) first, then open a PATH for cuts 1–3 (cut 4 optional/deferred per §6), each cut its own commit gated by the verification triple in §5.