proof(#2080): reserved-name dispatch seam (replaces false internal_-prefix helper premise)

[Th0rgal]

Summary

Phase 27 of the #2080 L2 proof tier. The previous slice assumed every helper in a runtime contract's internal-function table is internal_-prefixed. That premise is false for a real populated table: compiler helpers are named __verity_*, checked_*, panic_error_*, and template intrinsics — none internal_-prefixed. This PR replaces that false seam with the true reserved-name invariant.

• InternalTableNamesReserved generalizes InternalTableNamesInternalPrefixed: every decoded helper name is either internal_-prefixed or carries a known compiler-helper prefix (reservedInternalHelperPrefixes = [internal_, __verity_, checked_, panic_error_]). IsReservedInternalHelperName is Decidable.
• Consumers need only that the six ABI param-load builtins (calldataload, calldatasize, lt, revert, and, iszero) are not reserved (by decide) to obtain findInternalFunction? = none and hence genParamLoads calls-disjointness — so the invariant is dischargeable from actual compilation output.
• InternalTableNamesReserved_of_internalPrefixed lets the compiled-internal naming route still feed the new consumer seam; the _of_internalNamesPrefixed param-load lemma is rerouted through _of_reserved.
• Contract-level: reserved per-function seam compileFunctionSpec_correct_..._of_reserved, plus populated-table InternalTableNamesReserved_of_internalFunctions_append / _of_helpers_append_compiledInternalTable connectors.

Touched: IRInterpreter.lean, Function.lean, Contract.lean (+ regenerated PrintAxioms.lean, one signature-dominated allowlist entry in check_proof_length.py).

Base / dependency

Stacked on #2120 (paloma/issue-2080-populated-table-phase25c), which is stacked on #2119. Do not merge until the predecessor stack (#2119 → #2120) is merged/green. Rebase onto main once they land.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.{IRInterpreter,Function,Contract} — success (BUILD_EXIT=0, 1151/1151).
• python3 scripts/generate_print_axioms.py --check — OK (up to date).
• python3 scripts/check_proof_length.py — passed (reserved seam allowlisted, signature-dominated single-term body).
• git diff --check — clean.
• No new sorry / admit / axiom in touched proof files.

Refs #2080

---

Note

Low Risk
Proof-only Lean changes with no runtime or auth logic; risk is limited to theorem wiring and axiom inventory consistency.

Overview
Replaces the false premise that every runtime internal helper is internal_-prefixed with a reserved-name invariant (InternalTableNamesReserved / IsReservedInternalHelperName over internal_, __verity_, checked_, panic_error_), so populated tables with real compiler helpers can still discharge findInternalFunction? = none for ABI param-load builtins.

IRInterpreter.lean adds the reserved naming definitions, findInternalFunction?_eq_none_of_not_reserved, and InternalTableNamesReserved_of_internalPrefixed. Function.lean introduces genParamLoads_callsDisjoint_of_reserved and routes the old internal_-prefixed lemma through it. Contract.lean adds the per-function seam compileFunctionSpec_correct_..._of_reserved and renames/populates-table connectors to InternalTableNamesReserved_of_internalFunctions_append / _of_helpers_append_compiledInternalTable. PrintAxioms.lean and check_proof_length.py are updated for the new public theorems.

^{Reviewed by Cursor Bugbot for commit 6a005a2. 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 9:43am

[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_a288087f-d125-4060-9517-1e42b5cd2c70)