proof: package direct helper statement context bridge

[Th0rgal]

Summary

• add DirectInternalHelperStatementContextBridge, packaging supported source helper summary evidence with compiled helper dispatch for direct Stmt.internalCall and Stmt.internalCallAssign
• instantiate the bridge from SupportedBodyHelperInterface, SupportedBodyHelperSummariesSound, and SupportedRuntimeHelperTableInterface
• expose source-side direct helper call and assign evidence theorems, plus a compact assign-result/evidence wrapper for downstream head-step bridge proofs
• 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 " Compiler/Proofs/HelperStepProofs.lean PrintAxioms.lean (only generated audit comments report 0 sorry'd)

Issue #2080 Position

This does not close #2080 yet. It packages the supported-evidence handoff needed by the direct statement helper call/assign obligations, while leaving the actual with-internals head-step bridge proofs to consume this context together with the helper IR execution summary theorem from the parent PR.

[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 6:42am