proof: reserve compileValidatedCore helper segment

[Th0rgal]

Summary

• Add a yulFuncDefName? view plus simp facts for compiler-emitted dynamic-data, checked-arithmetic, panic, and related helper definitions.
• Prove the exact compileValidatedCore prebuilt helper segment satisfies the reserved-helper-name invariant, including template intrinsic helpers.
• Add InternalTableNamesReserved_of_compileValidatedCore_helpers_append_compiledInternalTable, which removes the caller-supplied helper-segment reserved-name premise from the populated internal-table seam while retaining the existing compiled-internal mapM premise.

Refs #2080

Base / dependency

Stacked on paloma/issue-2080-populated-table-phase25c because #2122 is still open and currently clean/green when inspected. This PR targets that branch.

Do not merge until predecessor stack is merged/green.

Validation

• git diff --check PASS
• lean-slot lake build Compiler.CompilationModel.DynamicData PASS
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract PASS
• python3 scripts/generate_print_axioms.py --check PASS
• python3 scripts/check_proof_length.py PASS
• no new sorry, admit, or axiom declarations in touched Lean files

Remaining #2080 gate

This closes the prebuilt helper-segment reserved-name proof for the current populated-table seam. The remaining gate is to thread the new helper-segment connector directly through the whole-contract dispatch retarget path from the concrete compileValidatedCore output, eliminating the remaining manual table-shape plumbing at the final consumer.

---

Note

Low Risk
Changes are confined to Lean proofs and metadata scripts; emitted Yul and compilation logic are unchanged aside from making compileSpecialEntrypoint public for the proof layer.

Overview
Adds yulFuncDefName? and @[simp] lemmas tying each compiler-emitted dynamic-data / checked-arithmetic / panic helper YulStmt to its reserved __verity_* (or related) name, so proofs can reason about helper lists without decoding IR by hand.

Introduces DecodedInternalHelperNamesReserved and a mirrored compileValidatedCoreHelperSegment definition, then proves that segment (including template intrinsic helpers from compileTemplateIntrinsicHelpers) satisfies the reserved-helper-name invariant. New connectors InternalTableNamesReserved_of_compileValidatedCore_helpers_append_compiledInternalTable and InternalTableNamesReserved_of_compileValidatedCore discharge InternalTableNamesReserved from a successful compileValidatedCore run instead of manual helper-segment plumbing.

compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_compileValidatedCore now feeds InternalTableNamesReserved_of_compileValidatedCore into the reserved-table seam (replacing the compiledInternalTable path). compileSpecialEntrypoint is exported (no longer private). PrintAxioms.lean and check_proof_length.py whitelist the new long proof theorems.

^{Reviewed by Cursor Bugbot for commit 84dfaa8. 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 10:14pm

[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_b1dccfa6-1271-47ba-85f1-6cdc50549c5c)

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 6155a4c0a9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[Th0rgal]

Review (automated, mission d4479a06): approved on content — merge blocked by predecessor stack.

Reviewed commit 6155a4c in an isolated worktree against base paloma/issue-2080-populated-table-phase25c:

• Diff is sound: 34 rfl simp name-lemmas in DynamicData.lean, segment-local DecodedInternalHelperNamesReserved composition lemmas, and the new public connector InternalTableNamesReserved_of_compileValidatedCore_helpers_append_compiledInternalTable correctly delegating to the existing helpers-append connector.
• Hygiene verified locally: git diff --check PASS, no new sorry/admit/axiom, scripts/check_proof_length.py PASS, scripts/generate_print_axioms.py --check PASS.
• No review threads; Bugbot skipped (usage limit) with no findings.
• Note: private compileTemplateIntrinsicHelpers_reserved is currently unused — acceptable staging for the next-phase consumer named in "Remaining proof(L2): Tier 2 — internal helper call preservation (close the 4 remaining interface goals) #2080 gate".
• CI: all checks green except build still in progress (started 16:27 UTC, full runs take ~70 min).

Blocker: predecessor landing PR #2122 is still open (base main, CLEAN, 25 commits). Per this PR's own directive, do not merge until the stack lands. Merging now would silently grow #2122 after creation/inspection.

Next action: merge #2122 to main first; GitHub will retarget this PR to main, then merge once its CI is green on the new base.

[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_68226512-d112-4307-ac4d-fa3ad3147097)

[Th0rgal]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 84dfaa85dc

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".