proof: expose direct helper fuel split interface

[Th0rgal]

Summary

Adds the reviewed direct-helper fuel split at the central singleton constructor layer:

• introduces pointwise bridge abbrevs for direct void and return-binding helper calls
• adds compiledStmtStepWithHelpersAndHelperIRWithInternals_internalCall_of_fuelSplitBridge
• adds compiledStmtStepWithHelpersAndHelperIRWithInternals_internalCallAssign_of_fuelSplitBridge

These keep the existing all-positive-fuel CompiledStmtStepWithHelpersAndHelperIRWithInternals target intact while exposing the two real proof obligations now visible after #2170:

• sufficient region: 1 < helperFuel and helperBodySize + 2 <= irFuel
• residual region: source-low-fuel or IR-insufficient-fuel

This is an explicit proof-interface review slice. It does not close the residual low/insufficient-fuel case and does not weaken the public single-step target.

Validation

• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.Calls
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• rg -n "\\bsorry\\b|\\badmit\\b|axiom |True :=|\\t" Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean PrintAxioms.lean

The final rg output only matches the standard PrintAxioms.lean audit comments.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 11, 2026 7:37am

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```