proof(#2080): land internal-helper preservation stack on main#2122
Merged
Conversation
…nals-retarget proof: route expr helper lists through WithInternals assembly
Introduce InternalTableNamesInternalPrefixed and findInternalFunction?_eq_none_of_not_internalPrefixed: a name that is not internal_-prefixed cannot resolve to any helper when the runtime contract's internal table satisfies the naming invariant. Forward-compatible replacement for the internalFunctions = [] disjointness route. Refs #2080
…nvariant Prove that the ABI parameter-load prologue emitted by genParamLoads (the min-input-size guard plus the per-param scalar loads) is disjoint from a runtime contract's internal-function table whenever the table satisfies InternalTableNamesInternalPrefixed. The six EVM/Yul builtins it emits (calldataload, calldatasize, lt, revert, and, iszero) are not internal_-prefixed, so none can resolve to a helper. Replaces the internalFunctions = [] route with a naming-invariant route that survives non-empty helper tables. Refs #2080
… seam Add compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_internalNamesPrefixed, which discharges the genParamLoads prefix-disjointness premise of its _of_body_goal sibling from the runtime contract's InternalTableNamesInternalPrefixed naming invariant instead of taking it as an opaque hypothesis. This is the selector-dispatch consumer seam that lets each per-function obligation feed straight into execIRFunctionWithInternals. Regenerate PrintAxioms.lean and allowlist the signature-dominated wrapper. Refs #2080
Adds the structural lemmas that let the whole-contract dispatch seam discharge the internal-table naming invariant instead of taking it as an opaque premise: - 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 those to the whole runtime internal table. Contract.lean gains the consumer seam compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_compiledInternalTable, which derives the naming invariant from the structural fact that every internal-table statement is a compileInternalFunction output, then delegates to the _of_internalNamesPrefixed sibling. Body is a single term application; allowlisted in check_proof_length.py for the mirrored premise list. PrintAxioms.lean regenerated: 5551 -> 5555 theorems, 0 sorry'd.
Package the structural premise that a runtime contract's internal-function table is generated by `compileInternalFunction`, then feed PR #2118's `_of_body_goal_of_compiledInternalTable` seam with that premise derived from the real compilation pipeline instead of taken as a hypothesis. New lemmas (Compiler/Proofs/IRGeneration/Contract.lean): - `compileInternalFunction_mapM_mem_exists`: every statement in the `internalFns.mapM compileInternalFunction` image is a `compileInternalFunction` output. Non-vacuous for a populated `internalFns`; no `internalFunctions = []` default-empty helper-world assumption. - `compiledInternalTable_of_internalFunctions_eq_mapM`: packages that image into the exact existential shape of the seam's `hcompiledTable` premise. - `compiledInternalTable_of_compileValidatedCore`: discharges the premise from a real `compileValidatedCore` output (currently via the SupportedSpec nil table). - `compileFunctionSpec_correct_generic_with_helper_proofs_and_helper_ir_of_body_goal_of_compileValidatedCore`: whole-contract dispatch consumer that invokes the #2118 seam with `hcompiledTable` discharged from the pipeline, so the runtime contract whose `execIRFunctionWithInternals` dispatch is proven is exactly the compiled one. Regenerated PrintAxioms.lean and allowlisted the signature-dominated consumer in check_proof_length.py (matching its `_of_compiledInternalTable` sibling). Refs #2080
…gment Add a reusable structural lemma `InternalTableNamesInternalPrefixed_of_internalFunctions_append` that distributes the internal-table naming invariant over a segmented `helpers ++ internalDefs` table (the shape `compileValidatedCore` actually emits), plus a consumer seam `InternalTableNamesInternalPrefixed_of_helpers_append_compiledInternalTable` that discharges the `internalFuncDefs` segment from the pipeline's `mapM` output and leaves only the helper-segment prefix obligation. This is the non-empty-table analogue of `compiledInternalTable_of_compileValidatedCore`, feeding the naming invariant consumed by the `internalNamesPrefixed` dispatch seam with no `internalFunctions = []` default-empty assumption. Refs #2080
…invariant (#2121) Introduce InternalTableNamesReserved as the true generalization of InternalTableNamesInternalPrefixed: decoded helper names are either internal_-prefixed OR a known compiler-helper prefix (__verity_, checked_, panic_error_). Consumers only need that the ABI param-load builtins (calldataload, calldatasize, lt, revert, and, iszero) are outside that reserved set to derive findInternalFunction? = none and the calls-disjoint fact, so the invariant is dischargeable from a real populated internal table. - IRInterpreter: reservedInternalHelperPrefixes, IsReservedInternalHelperName (+Decidable), InternalTableNamesReserved, findInternalFunction?_eq_none_of_not_reserved, InternalTableNamesReserved_of_internalPrefixed. - Function: genParamLoads_callsDisjoint_of_reserved; route the internalNamesPrefixed variant through it. - Contract: reserved-name per-function seam and populated-table append/pipeline connectors. Regenerate PrintAxioms.lean; allowlist the signature-dominated reserved seam. Refs #2080
Member
Author
|
@codex review |
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot 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_bcdf54f9-1615-48e6-81fa-85e586ecc993) |
|
Codex Review: Didn't find any major issues. Swish! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
Bugbot couldn't run - usage limit reachedBugbot 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_3e1a8a2b-15ff-4a20-b3bf-7bf25cb0d0ce) |
This was referenced Jul 8, 2026
Member
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Land the #2080 internal-helper preservation stack onto
mainafter the branch-stack PRs were merged into each other.This integrates the post-#2104 work that currently lives on
paloma/issue-2080-populated-table-phase25c, including:WithInternalsdirect/structural/function seams (proof: make scope lift helper-world parametric #2108/proof: add direct helper WithInternals interfaces #2111-proof(#2080): derive contract naming invariant from compiled internal table #2118)Why this PR exists
The stacked PRs are marked merged, but most were merged into their predecessor branches rather than into
main.mainis still behind the stack. This PR is the final integration gate to actually land the accumulated proof work onmain.Refs #2080.
Validation
To be performed by CI + review gate before merge.
Note
Medium Risk
Large additive formal verification surface touching compiler correctness and helper-aware execution; mistakes could admit unsound proofs, but changes extend parallel seams rather than rewriting proven legacy paths in place.
Overview
This PR lands the accumulated #2080 internal-helper preservation work onto
main: a parallel spec-functions /WithInternalsproof layer that compiles and executes againstspec.functionsinstead of the legacy empty-internal-helper world.Helper-step and list witnesses add
DirectInternalHelper*BridgeWithInternals, expression-head bridges (ExprInternalHelperHeadStepBridgeWithInternals), post-state companions for compositional helpers (includingExpr.add/Stmt.letVar), and assemblers that buildStmtList*WithInternalsinterfaces for direct calls, assigns, expression-position helpers, and structural heads (ite,forEach), culminating infullHelperAwareListWitnessWithInternals_of_allInterfaces.Generic induction and function bodies wire those witnesses through new
compileStmtList/ scope lemmas parameterized byinternalFunctions,exec_compileStmtList_generic_with_helpers_and_helper_ir_with_internals_*, mixed-list assembly inInterfaceAssembly, and body consumers such assupported_function_body_correct_from_exact_state_generic_split_helper_steps_and_helper_ir_with_internalsplussupported_function_body_with_internals_goal_of_compileFunctionSpec_with_internals.Contract / dispatch seam retargets per-function correctness to
execIRFunctionWithInternals: param-load prefix execution under internals,genParamLoads_callsDisjoint_of_reserved(and related naming lemmas), structural facts forcompileInternalFunctionmapMoutput, and wrappers that deriveInternalTableNamesReserved/ compiled-table premises fromcompileValidatedCoreand helper-segment++populated tables—so dispatch does not rely oninternalFunctions = []or hand-supplied disjointness.Reviewed by Cursor Bugbot for commit 99aae6f. Bugbot is set up for automated code reviews on this repo. Configure here.