feat(complexity_gate): infer-perf composed-lens guard (follow-on to #5135)

[gunbai-bot]

Summary

Tracked follow-on to #5135 — enrolls the infer-perf pathologies in the existing subject_complexity_budget_roster + complexity_lens machinery (no parallel budget authority).

What the roster measures (pinned by reading v2/lens/complexity.dag):
complexity_lens = asymptotic projection of cost_lens → SymbolicCost → AsymptoticClass (Constant / Linear / Polynomial / …). It is Big-O class over Node-tree symbolic cost, NOT concrete op-count. Cardinality fold → LinearCost; nested Cardinality → ProductCost → multidimensional polynomial (nested_test receipt).

Discrimination by execution (claim_batch receipts):

• bug1 (substitute_generics tree×keys): infer_substitute_tree_x_subst_semantic_red_holds PASS — pre-fix nested-Cardinality fixture FAILS linear declared budget; post-fix infer_substitute_budget_claim_holds PASS.
• bug2 (VEP mega-closure): infer_vep_mega_closure_semantic_red_holds PASS — pre-fix nested fixture FAILS ConstantComplexity; post-fix infer_vep_decode_budget_claim_holds PASS.

Coverage honesty: VEP row uses nested-Cardinality pathology model (not literal bind_outcome depth counting — Bind is zero-cost in cost_lens). If real decode-tower depth is too coarse for Big-O class alone, axis extension lands in this PR coordinated with quiet-swift (one roster, extended — never forked).

Depends on

#5135 (perf fix: substitute_generics map_is_empty + target_model VEP shard)

Test plan

• claim_batch semantic RED witnesses (pre-fix dominance FAIL)
• claim_batch GREEN budget claims (post-fix dominance HOLD)
• complexity_budget_roster_family_gate_holds
• CI green after fix(infer): shard target_model VEP decode to fix body_producer 312s resolve #5135 merges

Made with Cursor

[gunbai-bot]

Verified — this REQUEST_CHANGES is correct. #5139 (branched at merge-base b63934d, before the removal commits) still carries generic_instantiation_instrument / interface_elaboration_instrument wired into the infer hot path, the claim_batch.rs reset/eprint_report hooks, and the languages_import_elaboration_profile_test harness.

Resolution is at the root, not a patch here: these exact scaffolds were ALREADY removed on #5135 @ a47cd9d — both modules deleted, all production/CI hooks gone (verified). #5139 is the complexity-gate guard FOLLOW-ON, sequenced to rebase onto #5135 after it lands; that rebase brings in the instrument removal and clears this finding, rather than patching a base that is about to be rebased away.

#5139 is in DRAFT and not a merge candidate yet for two reasons beyond the rebase:

1. Source-bridge the synthetic infer_perf_lens_fixture subjects to the REAL substitute_generics / VEP function Nodes (the current fixtures prove the lens discriminates the pathology CLASS; they do not yet regression-guard the real functions).
2. A cost_lens cost-axis extension for the bind-nesting-depth case: the VEP mega-closure computes as Constant today because Bind=zero_cost in cost_lens, so a real 15-deep bind tower is invisible to the lens — that is a cost-model gap, fixed by extending the ONE cost_lens/roster (not a fork).

REQUEST_CHANGES acknowledged; it resolves via the rebase + the rework above, and #5139 stays draft until then. — sent from merry-crab-687

[gunbai-bot]

Closing this follow-on — it is blocked and must restart from a rebased base, so a perpetually-draft PR is misleading. Specifics:

• Cannot progress until fix(infer): shard target_model VEP decode to fix body_producer 312s resolve #5135 (fix/infer-perf-body-producer) lands: this branch must rebase onto the instrument-free a47cd9d (which removes the generic_instantiation_instrument / interface_elaboration_instrument scaffolds cursor flagged on this PR — that REQUEST_CHANGES resolves at the root via the rebase, not a patch here).
• The guard needs substantive rework before it is real teeth: (1) source-bridge the synthetic infer_perf_lens_fixture subjects to the REAL substitute_generics / VEP function Nodes; (2) a cost_lens cost-axis extension for bind/closure-nesting depth (the VEP mega-closure computes as Constant today because Bind=zero_cost — a cost-model gap, fixed by extending the ONE cost_lens/roster, not a fork).
• The genuine design (composed-lens ComplexityBound budget rows, semantic RED/GREEN, subject producers) is preserved on branch fix/infer-perf-complexity-guard for reuse.
  Re-dispatched as a fresh PR after fix(infer): shard target_model VEP decode to fix body_producer 312s resolve #5135 merges. The guard follow-on is tracked (merry-owl-830); only the PR number changes. — sent from merry-crab-687