nested-membership rewrite rule: nested-Cardinality O(n²) → single-Cardinality O(n)

[gunbai-bot]

Context

Follow-up to #5437 (cost-lens AlternativeCost floor + comprep bridge). Depends on that PR for comprep_source_resolved_root (the pipeline bridge). Rule 1 of the D2 complexity-reduction catalog.

What this adds

Rule: nested_membership (src/v2/lens/rewrite/nested_membership.dag)

Rewrites a nested Cardinality (outer wraps inner — O(n·m)) to a single Cardinality with the inner node's children hoisted directly (O(n)). Models: precompute the membership set once; replace the inner O(n) scan with O(1) lookup.

Precondition: outer has exactly one positional child (= inner Cardinality) and no Named children (no mutation coordinate in outer body — required for safe hoisting).

Test file: src/v2/lens/rewrite/nested_membership_test.dag — 4-witness matrix + pipeline guard:

• (a) rewrite fires: try_nested_membership_rewrite(nested_slow_input) = Present
• (b) class drop: ClassPolynomial(degree=2) → ClassLinear (cost_lens + complexity_lens both checked)
• (c) correctness: rewritten node's children == inner_card.children exactly
• (d) non-firing control: outer Cardinality with a Named edge → Absent
• (e) pipeline guard: comprep bridge resolves MVP1 loop source (bridge proved live as real consumer)

🟡 gap marker in src/v2/lens/cost.dag — records that Instantiation → unit_cost() (SequentialCost) means complexity_lens cannot produce ClassExponential for naive recursive functions. Blocks the naive-recursion→memoize rule detection. Dissolve-on: Instantiation base cost models recursion depth (new modeling, own runway).

Test polarities

• (a) goes RED without the try_nested_membership_rewrite function itself.
• (b) goes RED if cost_lens does not fold nested Cardinality to ProductCost(Linear, Linear).
• (d) goes RED if the Named-edge mutation-guard is absent (over-eager fire).
• (e) goes RED if any stage of the pipeline chain faults.

Grammar gap (documented)

MVP1 grammar cannot parse nested-loop source text (e.g., fn outer() -> Int { loop loop 1 }). Witnesses (a)-(d) use hand-constructed Node trees. Dissolve-on marker attached; grammar follow-up deferred.

Test plan

• cargo test --workspace passes
• cargo clippy --all-targets -- -D warnings clean
• All 5 test fns enrolled by CI floor naming convention (nested_membership_test.dag)
• Merge cost-lens: symbolic_max floor on AlternativeCost arm + per-fn subject-producer bridge #5437 first (dependency: comprep_source_resolved_root)

🤖 Generated with Claude Code

[gunbai-bot]

Paused, relocated to §5 post-stability per operator §3 reframe; branch session/proud-ferret-16-rule1 preserves nested_membership + the Instantiation→ExponentialCost gap marker for §5 pickup.