proofs: assign helper bridge catalog

[Th0rgal]

Summary

• project the helper-return-binding half of the complete per-callee helper bridge catalog
• let the existing assign-only list-interface assembler consume a full established catalog without exposing the unrelated void-call obligation
• refresh the generated axiom audit

This is the narrow second-interface catalog increment toward #2080.

Verification

• python3 scripts/generate_print_axioms.py --check
• git diff --check
• touched proof targets: LEAN_NUM_THREADS=2 lake build Compiler.Proofs.IRGeneration.GenericInduction.Calls Compiler.Proofs.HelperStepProofs
  • node: old-agent
  • job: adcc5d43-6373-4e52-a72b-41d463cc4162
  • exit: 0
  • head: 97ea15713c23a8ed4aef3d65f6fe20852cd1cdc5
  • receipt: exact_head
• full build: LEAN_NUM_THREADS=2 lake build
  • node: ashur
  • job: 62513330-efc7-4327-a125-e9f4c19a3ae3
  • exit: 0
  • head: 97ea15713c23a8ed4aef3d65f6fe20852cd1cdc5
  • receipt: exact_head
• axiom audit: LEAN_NUM_THREADS=2 lake build PrintAxioms
  • node: old-agent
  • job: 1cdd0437-23ce-4383-9e5d-316754965f87
  • exit: 0
  • head: 97ea15713c23a8ed4aef3d65f6fe20852cd1cdc5
  • receipt: exact_head

The known compiler-regressions OOM on current main is tracked in #2214 and is not a gate for this proof-only slice.

---

Note

Low Risk
Proof-only catalog plumbing with no runtime, auth, or compiler behavior changes.

Overview
Adds directInternalHelperPerCalleeAssignBridgeCatalog_of_bridgeCatalog, mirroring the existing call-only projection: from a full DirectInternalHelperPerCalleeBridgeCatalog, it yields the assign-only catalog by taking hbridge.assign, so assign-only list-interface assembly can reuse a full catalog without a void-call bridge obligation at the API boundary.

Registers the new lemma in PrintAxioms.lean (6026 public theorems).

^{Reviewed by Cursor Bugbot for commit 97ea157. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

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

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview	Jul 30, 2026 5:29pm

[github-actions]

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

[github-actions]

OpenCodeReview first-pass review

🟢 No findings from the OCR first pass. Advisory only.

No comments generated. Looks good to me.

OCR pilot metrics & packet coverage

OCR pilot metrics

• Routing: medium-lean (router-v10)
• Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 15 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status success; comments 0; files 2; tokens 51002; tool calls 10; warnings 0; duration 149s
• Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+12/-0), PrintAxioms.lean (+2/-1)

Pilot mode: advisory only. Codex Review remains the merge gate.