Complete pass-through overhead declarations so path composition is correct by construction, not by naming coincidence

[isPANN]

Background

Path overhead is composed by ReductionGraph::compose_path_overhead (src/rules/graph.rs), which folds each edge's ReductionOverhead with compose (substitute the previous edge's output expressions into the next edge's inputs). For this to work, each edge's overhead must declare every size field of its target problem that a downstream edge might read — including fields the reduction leaves unchanged (pass-through).

Some edges only declare the fields they actively change and omit the pass-through ones. When such an under-declaring edge sits in the middle of a path and a later edge reads an omitted field, compose finds no mapping for that field and leaves it symbolic, so it reads through to whatever same-named field exists on the source problem. The output is then correct only by coincidence — when the omitted name happens to be a real source field with the same meaning — and otherwise leaks a non-source variable.

This is the data-quality root cause underneath #1085. #1085 focuses on the observable Big-O leak (tseitin_*, num_encoding_bits) and on normalizing size-field names. This issue records the underlying incomplete pass-through declaration and the correct-by-coincidence fragility it creates, which is broader than the leak symptom (it also fires on paths where the read-through happens to land on a real source field).

Note: the growth-domain fix on branch 1075-growth-domain already makes the asymptotic front safe — an overhead variable that cannot be expressed in source variables is tainted to Unknown / O(?) rather than leaked (verified: pred path KSatisfiability QUBO no longer emits tseitin_*). This issue is about fixing the declarations so composition is correct by construction rather than relying on that taint safety net or on naming luck.

Concrete example (verified on 1075-growth-domain)

Path ExactCoverBy3Sets → MaximumSetPacking → ILP.

• src/rules/exactcoverby3sets_maximumsetpacking.rs:

  #[reduction(overhead = {
      num_sets = "num_subsets",
  })]
  

  Declares only num_sets. It omits universe_size, even though MaximumSetPacking has a universe_size() size field (src/models/set/maximum_set_packing.rs:120) and this reduction preserves the universe.

• src/rules/maximumsetpacking_ilp.rs:

  overhead = {
      num_vars = "num_sets",
      num_constraints = "universe_size",   // reads the field the previous edge never declared
  }
  

Composed result today:

pred path ExactCoverBy3Sets ILP  →  num_constraints = universe_size  =>  O(universe_size)

compose left universe_size symbolic and it read through to the source. This is correct here only because ExactCoverBy3Sets happens to declare a universe_size size field (declared_size_fields(ExactCoverBy3Sets) = {num_sets, num_subsets, universe_size}) that means the same thing. Measured cross-check (direct edge, universe_size = 6): the real constructed ILP has 7 constraints and the direct-edge formula universe_size + 1 = 7 — consistent, so the semantics are right; the multi-hop path only renders right by naming coincidence.

Why it is fragile / where it breaks

If the omitted field's name is not a source size field (the CircuitSAT → Satisfiability route that drops num_literals, or the tseitin_* / num_encoding_bits derived getters in #1085), the read-through produces a non-source variable — the leak #1085 describes. And a naive step-by-step evaluate_output_size predictor over the same path drops the undeclared field to 0 mid-chain, diverging from the symbolic compose_path_overhead read-through. The proof harness (branch 1075-growth-domain, src/unit_tests/overhead_composition_proof.rs, not merged) counted 219 such ill-formed multi-hop paths where an edge reads a size field the previous edge never declared.

The measured Pareto search is not affected (it re-measures the real instance at each hop), and the growth-domain front is safe (taints to O(?)). The impact is on compose_path_overhead's symbolic output (display / pred path overall overhead), which is correct-by-coincidence on these paths.

Proposed fix

Complete the pass-through declarations: every edge overhead should declare each of its target problem's size fields, mapping unchanged fields to themselves. For the example:

#[reduction(overhead = {
    num_sets      = "num_subsets",
    universe_size = "universe_size",   // reduction preserves the universe
})]
impl ReduceTo<MaximumSetPacking<One>> for ExactCoverBy3Sets { ... }

Then compose maps the field explicitly instead of relying on read-through, and the symbolic and step-by-step predictors agree. This also removes a chunk of the size_field_names name-pollution #1085 is fighting.

Verification

• For every registered reduction edge, assert its ReductionOverhead declares a mapping for every declared size field of its target problem (a static completeness check over the inventory — could live next to the existing overhead tests).
• Re-run the (unmerged) p1_real_paths_compose_equals_chained check from the proof harness: after completing declarations, the illformed_paths count should drop to 0 (currently 219), i.e. compose_path_overhead and the step-by-step evaluate_output_size chain agree on every well-formed input.

Negative control: on current main, compose leaves universe_size symbolic on ExactCoverBy3Sets → MaximumSetPacking → ILP (no explicit mapping from the first edge) — confirming the declaration is incomplete before the fix.

Relationship to other issues

• Normalize size-field names across reductions so composed asymptotic Big-O is always in source variables #1085 — normalize size-field names so composed Big-O stays in source variables (the leak symptom). Same root cause; this issue is the declaration-completeness angle and the correct-by-coincidence cases that don't leak.
• Calibrate reduction overhead formulas against measured reduction behavior (approach TBD) #1082 — overhead formula/coefficient calibration (magnitudes). Out of scope here; this issue is purely about which fields are declared, not their formulas.