proof: retarget whole-contract helper IR from core output

[Th0rgal]

Summary

• Adds legacyCompatibleRuntimeContract_of_compileValidatedCore, packaging the concrete compileValidatedCore = Except.ok ir output into the closed helper-aware runtime compatibility shape.
• Adds compile_preserves_semantics_with_helper_proofs_and_helper_ir_of_compileValidatedCore, a whole-contract retarget connector that consumes interpretIRWithInternals for the compiled runtime contract without a manual hhelperIR equality.
• Regenerates PrintAxioms.lean for the two new public theorem entries.

Stack / base

• Base: paloma/issue-2080-helper-segment-reserved-names-phase28
• Stacked on proof: reserve compileValidatedCore helper segment #2124, transitively on proof(#2080): land internal-helper preservation stack on main #2122.
• proof: package compileValidatedCore table shape #2125 is already merged into the phase-28 branch tip used here.

Do not merge until predecessor stack is merged/green.

Validation

• git diff --check - passed
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract - passed
• lean-slot lake build PrintAxioms - passed (pre-existing warnings only in unrelated modules)
• python3 scripts/generate_print_axioms.py --check - passed
• python3 scripts/check_proof_length.py - passed
• Strict added-placeholder scan over touched files found no new sorry, admit, or axiom declarations.

Remaining #2080 gate

This slice removes the raw whole-contract hhelperIR equality at the validated-core connector. The remaining closure is to derive LegacyCompatibleExternalBodies ir (or preferably the weaker disjoint external-body runtime condition) directly from the concrete compileValidatedCore external-function compilation output, so the connector has no external-body compatibility premise.

Refs #2080

---

Note

Low Risk
Proof-only changes in compiler IR generation lemmas and axiom inventory; no executable compiler, auth, or data-path behavior.

Overview
Adds Lean proof plumbing so whole-contract helper-aware correctness can be stated from a concrete compileValidatedCore = Except.ok ir result instead of a hand-written interpretIRWithInternals = interpretIR equality.

legacyCompatibleRuntimeContract_of_compileValidatedCore combines the pipeline fact that supported specs yield an empty internal table with LegacyCompatibleExternalBodies into LegacyCompatibleRuntimeContract, matching what the closed conservative-extension theorems expect.

compile_preserves_semantics_with_helper_proofs_and_helper_ir_of_compileValidatedCore is the validated-core entry point: it rebuilds CompilationModel.compile = Except.ok ir from validation + core, feeds the legacy runtime witness above, and uses the already-closed interpretIRWithInternalsZeroConservativeExtensionGoal_closed path—callers no longer supply hhelperIR manually. LegacyCompatibleExternalBodies ir remains an explicit premise (not yet derived from compilation output).

PrintAxioms.lean is regenerated to list the two new public theorems.

^{Reviewed by Cursor Bugbot for commit 3f11865. 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 9, 2026 4:37am

[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_7208ce47-4829-453e-a0ed-e83b1bbc57ec)

[Th0rgal]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: 3f11865460

ℹ️ 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".