proof(#2080): naming-invariant param-load disjointness contract seam

[Th0rgal]

Base / dependency (stacked)

• Base branch: paloma/issue-2080-function-exec-withinternals (head of PR proof: bridge function exec with internals #2116).
• Stack: proof: bridge function exec with internals #2116 → paloma/issue-2080-function-withinternals-bridge. proof: bridge function exec with internals #2116 is OPEN, MERGEABLE, all checks green at time of writing.
• Do not merge until predecessor stack (proof: bridge function exec with internals #2116 and below) is merged/green.

Summary

Threads the L2 param-load prefix-disjointness fact through to the selector-dispatch consumer seam, reducing reliance on conservative-extension / default-empty helper-world wrappers.

• IRInterpreter.lean: add InternalTableNamesInternalPrefixed (contract invariant: every internal-table entry's name carries the internal_ prefix) and findInternalFunction?_eq_none_of_not_internalPrefixed (a non-prefixed name never resolves in the internal table).
• Function.lean: prove genParamLoads call-disjointness from the internal table out of per-builtin findInternalFunction? = none facts (genScalarLoad / genParamLoadBodyFrom recursion + minInputSizeCheck), then package it as genParamLoads_callsDisjoint_of_internalNamesPrefixed, which supplies those facts from the naming invariant via by decide on each builtin's non-internal_ prefix.
• Contract.lean: add compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_internalNamesPrefixed — same premises as its _of_body_goal sibling except it discharges the hparamDisjoint premise from InternalTableNamesInternalPrefixed (param supportedness comes from SupportedSpec via supported_params_of_supportedSpec). Each per-function obligation now feeds straight into execIRFunctionWithInternals without an opaque disjointness witness.

The naming-invariant route (rather than internalFunctions = []) is deliberately forward-compatible with non-empty helper tables — the direction #2080 wants to move.

Validation

All run via lean-slot (host-wide gate, Spark offload), from verity/:

• lean-slot lake build PrintAxioms → Build completed successfully. Whole-tree axiom gate (PrintAxioms imports every top-level theorem to #print axioms); Contract.lean's new theorem and all downstream modules compile. Every printed axiom is standard (propext, Classical.choice, Quot.sound) — no sorryAx.
• Individual green builds this slice: IRInterpreter, Function, Contract.
• python3 scripts/generate_print_axioms.py --check → OK: PrintAxioms.lean is up to date.
• python3 scripts/check_proof_length.py → passed (the signature-dominated wrapper is allowlisted with justification; body is a single term application).
• git diff --check → clean.
• No new sorry / admit / axiom in any touched proof file.

Next slice (not in this PR — kept narrow)

Whole-contract dispatch integration: establish InternalTableNamesInternalPrefixed for the compiled runtime contract from the compilation pipeline, and supply the per-function body-preservation goal, so the whole-contract theorem consumes this seam across all selector-dispatched functions and fully retires the default-empty helper-world wrapper.

Refs #2080

---

Note

Low Risk
Lean proof-only changes with no runtime or auth logic; risk is limited to proof maintenance and axiom/theorem registration consistency.

Overview
Adds a forward-compatible proof path so genParamLoads ABI prefix code cannot collide with internal helpers when the runtime table is non-empty, as long as every helper name carries the internal_ prefix.

IRInterpreter: introduces InternalTableNamesInternalPrefixed and findInternalFunction?_eq_none_of_not_internalPrefixed so non-prefixed names (EVM/Yul builtins) never resolve in the internal table.

Function: proves genParamLoads call-disjointness from per-builtin findInternalFunction? = none lemmas, then packages it as genParamLoads_callsDisjoint_of_internalNamesPrefixed using the naming invariant.

Contract: adds compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_internalNamesPrefixed, mirroring the existing _of_body_goal wrapper but replacing opaque hparamDisjoint with InternalTableNamesInternalPrefixed (param support from SupportedSpec).

Tooling: registers new theorems in PrintAxioms.lean and allowlists the long signature-only contract wrapper in check_proof_length.py.

^{Reviewed by Cursor Bugbot for commit 5759254. 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 4:25pm

[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_842b1df5-9db6-4d04-8612-c99cb1c86fbf)