Proof: model IR internal helper composition for the generic Layer 2 theorem

[Th0rgal]

Summary

SupportedSpec and the Layer 2 theorem surface are now helper-proof-ready on the source side, but the compiled-side IR semantics still cannot execute internal helper calls. execIRFunction only runs the compiled external function body and ignores IRContract.internalFunctions, so any generic helper-summary composition proof remains blocked even after the source-side summary/rank interfaces exist.

This issue tracks the compiled-side theorem target and proof architecture needed to make internal helper composition a real generic Layer 2 capability instead of a fail-closed exclusion.

Why this is the next structural blocker

PR #1633 split the body witness into feature-local interfaces and added:

• positive direct-callee helper-summary inventory (SupportedBodyHelperInterface.summaryOf)
• a decreasing helper-rank interface (calleeRanksDecrease)
• helper-aware source semantics (evalExprWithHelpers, execStmtListWithHelpers, interpretInternalFunctionFuel)
• theorem-level proof wrappers (SupportedSpecHelperProofs)

What still blocks end-to-end generic helper reuse:

1. SupportedStmtList still excludes helper-call syntax, so generic body proofs do not yet admit helper forms.
2. GenericInduction.supported_function_body_correct_from_exact_state_generic_with_helpers still collapses helper-aware source semantics back to helper-free semantics through calls.helperCompatibility.
3. Compiler.Proofs.IRGeneration.IRInterpreter.execIRFunction does not model internal helper call composition at all.

The third point is the compiled-side blocker. Without an IR semantics that can execute helper calls, consuming source-side helper summaries alone would not strengthen compile_preserves_semantics for helper-using contracts.

Scope

• define the exact IR semantics target for internal helper composition
• make the target compatible with the existing generic theorem surface, ideally via helper-aware/contract-aware IR execution plus compatibility lemmas on the current helper-free fragment
• preserve proof genericity: no contract-specific helper assumptions, no demo-only shortcuts
• keep the trusted boundary explicit if any temporary compatibility reduction remains

Candidate implementation shape

• add contract-aware IR execution that can resolve calls against IRContract.internalFunctions
• introduce explicit fuel / rank discipline for internal helper execution on the IR side, aligned with the source-side decreasing helper-rank interface
• retarget the generic theorem stack to the richer IR semantics family while proving equivalence to the current execIRFunction / interpretIR on the existing supported fragment
• only then thread helper-summary soundness/rank evidence through the body proof to remove SupportedBodyCallInterface.helperCompatibility

Acceptance criteria

• the remaining helper blocker is no longer "IR semantics has no internal helper composition"
• the exact compiled-side theorem target for helper-using contracts is encoded in code/docs, not only in prose
• the public Layer 2 theorem surface does not need another theorem-shape rewrite when helper composition is proved
• docs and artifacts/layer2_boundary_catalog.json link to this issue as the compiled-side helper blocker

Part of #1630.
Related: #1510, #1633.

[Th0rgal]

PR #1639 now lands the compiled-side helper execution target in code via IRInterpreter.execIRFunctionWithInternals / IRInterpreter.interpretIRWithInternals. That reduces #1638 from "no helper-aware IR target exists" to proof retargeting: the remaining work is to move the body/dispatch/contract preservation lemmas onto that target and consume helper-summary soundness/rank evidence so calls.helperCompatibility can disappear.

[Th0rgal]

Follow-up on proof/ir-helper-semantics-target after commit 1b01d5a5.

The compiled-side blocker is now pinned down more precisely in the machine-readable Layer 2 boundary catalog and synced docs:

• the blocker is no longer described only as "retarget the theorem stack to interpretIRWithInternals"
• the immediate missing proof step is now explicit: prove interpretIRWithInternals is a conservative extension of legacy interpretIR on the legacy-compatible external-body Yul subset generated by today's supported fragment
• only after that compatibility seam is formalized should the body/dispatch/contract theorems be retargeted to execIRFunctionWithInternals / interpretIRWithInternals, and then helper-summary soundness/rank evidence can replace calls.helperCompatibility

This keeps the current trusted boundary unchanged while making the next proof obligation auditable in CI (artifacts/layer2_boundary_catalog.json, sync checks, and docs).

[Th0rgal]

Update from proof/ir-helper-semantics-target (9ac8dc9d): the compiled-side blocker in #1638 is now sharpened one step further.

The repo already had:

• a helper-aware compiled execution target (execIRFunctionWithInternals, interpretIRWithInternals)
• a formalized helper-free compatibility subset (LegacyCompatibleExternalStmtList)
• an explicit helper-free runtime-contract target (Dispatch.runtimeContractOfFunctions with internalFunctions = [])

What is now recorded explicitly in code/docs/catalog is the proof-surface blocker underneath the next theorem step:

• the current helper-aware compiled semantics is still exposed only through opaque partial def executables
• so the first conservative-extension theorem needs a theorem-friendly total or inductive mirror of that target rather than proving directly against the executable surface

This does not change the trusted boundary or widen the proved fragment. It makes the next missing seam machine-readable in artifacts/layer2_boundary_catalog.json and synced docs, so the follow-on proof PR can target the right abstraction boundary instead of discovering the opacity problem mid-proof.

[Th0rgal]

Status Update: Prioritized Roadmap for Full Helper Support

PR #1639 has made significant progress on the compiled-side helper composition architecture. Here is the current coverage and a prioritized roadmap for what remains.

What's Done (PR #1639)

IR Semantics Infrastructure:

• execIRStmtWithInternals / evalIRExprWithInternals / evalIRCallWithInternals — full helper-aware IR interpreter with fuel-based recursion
• execIRInternalFunctionWithInternals — internal function execution with variable setup, body execution, and return value extraction
• Conservative extension proofs: both _of_callsDisjoint and _of_no_internal variants, proving the new semantics agrees with legacy execIRStmt on helper-free code
• Disjointness predicates (yulExprCallsDisjointFromInternalTable, YulStmtListCallsDisjointFromInternalTable) with full inductive coverage including switch_/for_

Void-Call Semantic Gap Fix (commit 686de35):

• execIRStmtWithInternals .expr (.call func args) now dispatches to evalIRCallWithInternals directly, so void internal helpers (returning 0 values) succeed instead of reverting through evalIRExprWithInternals's single-value filter
• Updated all conservative extension proofs for the new definition structure

Positive Helper-Call Characterization:

• evalIRCallWithInternals_of_internal_function — call-level reduction to execIRInternalFunctionWithInternals
• execIRStmtWithInternals_letMany_call_internal — stmt-level for Stmt.internalCallAssign
• execIRStmtWithInternals_expr_call_internal — stmt-level for Stmt.internalCall (void)
• Singleton list versions and end-to-end compilation bridges for both variants

Step Interface Architecture:

• CompiledStmtStepWithHelpersAndHelperIR structure with compileOk + preserves
• compiledStmtStepWithHelpersAndHelperIR_internalCallAssign — generic step constructor parameterized by bridge hypothesis
• compiledStmtStepWithHelpersAndHelperIR_internalCall — same for void calls
• Four helper surface interfaces (call, assign, expr, structural) with vacuous constructors via helperSurfaceClosed

Source-Side Foundations:

• findUniqueInternalFunction?_of_witness + public characterization theorems
• functionNamesNodup field on SupportedSpecInvariants
• Compilation shape extraction (compileStmt_internalCallAssign_shape, compileStmt_internalCall_shape)
• findInternalFunction?_of_compileInternalFunction_mem bridge

---

Prioritized Roadmap

Tier 1 — Core Helper Call Wiring (enables first concrete helper-using contract)

Status: Partially complete. Step constructors exist; bridge hypotheses need instantiation.

1. Fix void-call semantic gap ✅ Done (686de35)
2. Add IR characterization for Stmt.internalCall ✅ Done (686de35)
3. Wire non-vacuous StmtListDirectInternalHelper{Assign,Call}StepInterface — instantiate the bridge hypothesis in the generic step constructors with actual per-helper-rank induction. This requires:
   • A rank-indexed induction scheme on SupportedBodyHelperInterface.calleeRanksDecrease
   • Per-rank source↔IR bridge: tie execStmtWithHelpers to execIRStmtsWithInternals for each helper call site
   • The bridge hypothesis in the step constructors is already parameterized for this
4. Expression-position helper calls (Expr.internalCall) — add evalIRExprWithInternals_call_internal characterization and wire through StmtListExprInternalHelperStepInterface
5. ite/forEach structural support — extend StmtListStructuralInternalHelperStepInterface for helpers called inside conditionals and loops

Tier 2 — Storage Pattern Extensions (needed for real-world contracts)

6. Storage mapping slot composition — prove helper calls inside sstore(.call "mappingSlot" ...) compose correctly
7. Packed storage fields — readPacked/writePacked helper composition through the packed field abstraction layer

Tier 3 — Advanced Features

8. Events and errors — helpers that emit events or revert with custom errors
9. Constructor support — helper calls in deployment/constructor code paths
10. Multi-return helpers — helpers returning >1 value (currently only 0 and 1 are characterized)

Tier 4 — Out of Scope for This Issue

11. External calls — cross-contract calls are a separate trust boundary
12. Dynamic dispatch — function-pointer-like patterns

---

Key Architectural Notes

• The step interface split (call/assign/expr/structural) is designed so each tier can be independently advanced without blocking others
• The helperSurfaceClosed vacuous path remains valid for helper-free contracts — no regression
• The bridge hypothesis pattern in the step constructors cleanly separates the "prove the step exists" concern from "prove the bridge holds for this specific helper"
• internalFunctionYulName naming convention means helper function names never collide with builtins (stop/sstore/mstore/revert/return), which the characterization theorems exploit

Files of Interest

• IRInterpreter.lean — IR semantics + characterization chain (~3800 lines)
• GenericInduction.lean — step interfaces + generic induction (~7100 lines)
• SourceSemantics.lean — source-side helper execution + public characterizations
• SupportedSpec.lean — SupportedSpecInvariants with functionNamesNodup

[Th0rgal]

Closing as part of issue tracker cleanup. The work tracked here has been consolidated into new focused tracking issues. See the new issues for updated scope and status.