proof(#2080): derive contract naming invariant from compiled internal table

[Th0rgal]

Summary

Threads the runtime contract's internal-table naming invariant into the whole-contract dispatch seam by deriving it from the structural compilation fact — every internal-table statement is a compileInternalFunction output — instead of taking InternalTableNamesInternalPrefixed as an opaque hypothesis.

Stacked on top of paloma/issue-2080-selector-dispatch-withinternals (PR #2117's WithInternals selector seam).

New lemmas (Compiler/Proofs/IRGeneration/Function.lean)

• internalFunctionYulName_take_prefix — a compiled internal helper's Yul name carries the internal_ prefix.
• compileInternalFunction_isFuncDef_internalNamed — a compileInternalFunction output is a FunctionDefinition whose name is internal_-prefixed.
• InternalTableNamesInternalPrefixed_of_all_compiledInternal — lifts the above to the whole runtime internal table.

New consumer seam (Compiler/Proofs/IRGeneration/Contract.lean)

• compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_compiledInternalTable — takes the structural "all internal-table stmts are compiled internal helpers" premise, derives the naming invariant, and delegates to the _of_internalNamesPrefixed sibling. The body is a single term application; the length is entirely the mirrored premise list (allowlisted in check_proof_length.py).

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.Function — green
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract — green (1144/1144, with the new seam)
• lean-slot lake build Compiler.Proofs.HelperStepProofs — green (1139/1139)
• python3 scripts/generate_print_axioms.py --check — OK (5551 -> 5555 theorems, 0 sorry'd)
• python3 scripts/check_proof_length.py — pass
• git diff --check — clean
• No new sorry/admit/axiom in touched proof files
• lake build PrintAxioms — running in CI (constructive proofs only; no new axioms expected)

Test plan

• CI green (full lake build, PrintAxioms axiom footprint, proof-length gate)

Do not merge until the base PR lands.

---

Note

Low Risk
Lean proof-only changes with no runtime or auth logic; risk is limited to proof maintenance and CI gates (PrintAxioms, proof length).

Overview
Adds proof plumbing so whole-contract helper-aware correctness can assume every runtime internal-table stmt came from compileInternalFunction, instead of supplying InternalTableNamesInternalPrefixed by hand.

In Function.lean, three lemmas chain compilation shape to naming: internalFunctionYulName_take_prefix, compileInternalFunction_isFuncDef_internalNamed, and InternalTableNamesInternalPrefixed_of_all_compiledInternal.

In Contract.lean, compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_compiledInternalTable mirrors the _of_internalNamesPrefixed wrapper but takes hcompiledTable and derives the naming invariant before delegating to execIRFunctionWithInternals (no manual param-load disjointness witness).

PrintAxioms.lean and check_proof_length.py register the new public theorem (+4 lemmas, allowlist entry).

^{Reviewed by Cursor Bugbot for commit 455906f. 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 7, 2026 6:07pm

[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_92a49885-92f5-4b23-b053-80ff107b34ad)

[Th0rgal]

Review (automated) — commit 455906ff

Reviewed the single-commit diff in an isolated worktree. Proof content looks sound and merge-ready in isolation:

• Function.lean — three new lemmas are coherent and non-vacuous:
  • internalFunctionYulName_take_prefix — structural fact that a compiled helper's Yul name carries the internal_ prefix.
  • compileInternalFunction_isFuncDef_internalNamed — mirrors compileInternalFunction_ok_components' case analysis to extract the emitted name.
  • InternalTableNamesInternalPrefixed_of_all_compiledInternal — lifts the above to the whole runtime internal table via filterMap/irInternalFunctionDefOfStmt?. This derives the naming invariant from the real compilation fact rather than hiding the proof(L2): Tier 2 — internal helper call preservation (close the 4 remaining interface goals) #2080 gate behind a vacuous/empty-table assumption.
• Contract.lean — ..._of_compiledInternalTable is a single term application delegating to the existing ..._of_internalNamesPrefixed sibling; the new hcompiledTable premise is a genuine structural obligation, not a soundness hole.
• check_proof_length.py — one narrow, justified allowlist entry (signature-dominated wrapper, single-term body).
• PrintAxioms.lean — regeneration consistent: 5551 → 5555 (+4 public), 0 sorry'd. No new sorry/admit/axiom introduced; git diff --check clean.

Merge blocker: this PR is stacked on #2117 (paloma/issue-2080-selector-dispatch-withinternals), which is still open/unmerged (its own base is paloma/issue-2080-function-exec-withinternals). Per the stacked-PR policy this slice must not be merged into an open predecessor branch ahead of bottom-up landing. CI core checks (build, checks, changes) are green; build-audits and build-compiler-binaries were still running at review time. No review threads; Cursor Bugbot reported "couldn't run — usage limit reached" (no findings, not a resolvable thread).

Next step: land the predecessor stack (#2117 and below) first, then re-target/merge this slice.