proof: add direct helper sufficient fuel adapters

[Th0rgal]

Summary

• add directInternalHelperExtraFuel, the explicit inverse offset for internalHelperCallFuel
• expose sufficient-fuel adapters for direct statement helper calls:
  • directInternalHelperStatementContextBridge_callStepMatch_of_sufficientFuel
  • directInternalHelperStatementContextBridge_assignStepMatch_of_sufficientFuel
• these re-index the exact-fuel proof: expose direct helper summary step match interface #2169 direct step-match theorems to statement-level helper fuel and arbitrary IR fuel when:
  • 1 < stmtHelperFuel
  • sizeOf helper.body + 2 <= irFuel
• refresh PrintAxioms.lean for the two new public proof declarations

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs
• 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/HelperStepProofs.lean PrintAxioms.lean (only generated audit comments report 0 sorry'd)

Issue #2080 Position

This still does not close #2080. It makes the remaining direct head-step fuel gap explicit: the helper-body summary path covers the sufficient-fuel region, while the existing direct head-step bridge asks for all positive statement fuel and all wrapper IR fuel. The next proof/interface review must account for the low-fuel cases or strengthen the public head-step fuel contract.

[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:14am