proof(#2080): split populated internal-table naming invariant over helper segment

[Th0rgal]

Summary

Tier-2 internal-helper-call preservation (proof/L2) for #2080. This slice
generalizes the compiled-internal-table naming machinery from the pure
mapM-image table to the populated table shape that
compileValidatedCore actually emits, namely
<prebuilt helper segments> ++ internalFuncDefs
(see internalFunctions := in Compiler/CompilationModel/Dispatch.lean).

Two additions in Compiler/Proofs/IRGeneration/Contract.lean:

• Reusable structural lemma InternalTableNamesInternalPrefixed_of_internalFunctions_append:
  distributes InternalTableNamesInternalPrefixed over a segmented
  helpers ++ internalDefs internal table via List.mem_append, so the
  whole-table naming obligation splits into two independent per-segment
  obligations (helper segment + internalFuncDefs segment). Proved
  without any filterMap-append rewriting.

• Consumer seam InternalTableNamesInternalPrefixed_of_helpers_append_compiledInternalTable:
  for a contract whose internal table is helpers ++ internalDefs with
  internalDefs the compileInternalFunction mapM image, derives
  InternalTableNamesInternalPrefixed — discharging the internalFuncDefs
  segment structurally from the pipeline's mapM equation
  (compileInternalFunction_mapM_mem_exists +
  Function.InternalTableNamesInternalPrefixed_of_all_compiledInternal)
  and leaving only the helper-segment prefix obligation for a later slice.
  This is the non-empty-table analogue of
  compiledInternalTable_of_compileValidatedCore, feeding the naming
  invariant consumed by
  ..._of_body_goal_of_internalNamesPrefixed with no
  internalFunctions = [] default-empty assumption.

PrintAxioms.lean regenerated to register the two new public theorems
(0 sorry'd).

Base / dependency / stack

• Base: paloma/issue-2080-dispatch-compiled-internal-table (PR proof(#2080): feed compiled-internal-table dispatch seam from pipeline output #2119, still open).
• Stacked on proof(#2080): feed compiled-internal-table dispatch seam from pipeline output #2119. Do not merge until the predecessor stack (proof(#2080): feed compiled-internal-table dispatch seam from pipeline output #2119) is merged/green.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.Contract -> ✔ [1144/1144] Built ... Build completed successfully.
• python3 scripts/generate_print_axioms.py --check -> OK: PrintAxioms.lean is up to date.
• python3 scripts/check_proof_length.py -> passed (no new proof over the 50-line hard limit).
• git diff --check -> clean.
• No new sorry/admit/axiom in touched proof files.

Refs #2080

---

Note

Low Risk
Proof-only additions in IR generation contract lemmas plus axiom index regeneration; no runtime or compilation behavior changes.

Overview
Adds proof infrastructure so InternalTableNamesInternalPrefixed can be shown for the populated internal table shape helpers ++ internalFuncDefs that compileValidatedCore emits, not only a pure mapM image.

InternalTableNamesInternalPrefixed_of_internalFunctions_append splits the whole-table naming obligation into independent per-segment checks via List.mem_append, without filterMap-append rewriting.

InternalTableNamesInternalPrefixed_of_helpers_append_compiledInternalTable is the consumer seam: given internalFunctions = helpers ++ internalDefs and a successful compileInternalFunction mapM, it proves the invariant when the helper segment is already prefix-correct—the internalDefs side is discharged from existing mapM / compiled-internal lemmas. That feeds the same naming premise used by ..._of_body_goal_of_internalNamesPrefixed without assuming an empty internal table.

PrintAxioms.lean registers both new public theorems (count 5561 → 5563).

^{Reviewed by Cursor Bugbot for commit f8e8295. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 8, 2026 2:15am

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_ff78713d-2f94-440b-b58b-6fdc80975bde)