fix: ensure vk is compatible with recursion circuit check

[zlangley]

• generalize recursion circuit to use max_interactions from vkey
• ensure that the recursion circuit can actually be built for the child vkey in construction

[jonathanpwang]

@claude explain where max_interactions is used in the proof shape AIR constraints

[claude]

Claude finished @jonathanpwang's task in 1m 26s —— View job

---

• Read the changed files in this PR
• Trace max_interactions through the proof shape AIR constraints
• Write up explanation

Where max_interaction_count is used in the proof shape AIR constraints

max_interaction_count flows through the system in two places: (1) an AIR constraint that enforces the total interaction count is bounded, and (2) a construction-time assertion that the recursion circuit can enforce all child VK trace height constraints.

---

1. AIR constraint: bounding total interactions (summary row)

The core constraint lives in ProofShapeAir::eval() at crates/recursion/src/proof_shape/proof_shape/core.rs:1241-1277.

On the summary row (is_last = 1), the AIR constrains that total_interactions < max_interaction_count. Here's how:

1. The total_interactions_limbs column accumulates sum(num_interactions_per_row[i] * lifted_height[i]) across all present AIRs (lines 1084-1112). This is a running sum with carry propagation across NUM_LIMBS=4 limbs of LIMB_BITS=8 bits each.

2. On the summary row, the max_interaction_count is decomposed into limbs:

   // core.rs:1250-1251
   let max_interactions =
       decompose_f::<AB::Expr, NUM_LIMBS, LIMB_BITS>(self.max_interaction_count as usize);

3. A diff_marker array (reusing the num_interactions_limbs column on summary rows) marks the most significant limb index where max_interactions and total_interactions_limbs differ (lines 1255-1267).

4. The constraint enforces prefix == 1 (exactly one diff_marker is set) and then range-checks max_interactions[diff_idx] - total_interactions_limbs[diff_idx] - 1 to be in [0, 256) (lines 1269-1277). This proves the strict inequality total_interactions < max_interaction_count at the first differing limb (from MSB), because:

   • All higher limbs are equal (enforced by the prefix/marker logic)
   • At the differing limb, p[i] - t[i] - 1 >= 0 means p[i] > t[i]

Before this PR, max_interactions was hardcoded to F::ORDER_U32 (the BabyBear prime ~2^31), meaning the constraint was vacuous. This PR changes it to use self.max_interaction_count from the VK, making it a meaningful bound.

The same fix is applied in trace generation (core.rs:414-416) and the CUDA kernel (air.cu:260, previously Fp::P, now max_interaction_count).

---

2. Construction-time check: VK compatibility (system/mod.rs:503-524)

This is the new assertion added by this PR. At VerifierSubCircuit construction:

let proof_shape_constraint = LinearConstraint {
    coefficients: child_mvk.inner.per_air.iter()
        .map(|avk| avk.num_interactions() as u32).collect(),
    threshold: child_mvk.inner.params.logup.max_interaction_count,
};
for (i, constraint) in child_mvk.inner.trace_height_constraints.iter().enumerate() {
    assert!(constraint.is_implied_by(&proof_shape_constraint), ...);
}

This checks that the single linear constraint enforced by the proof shape AIR (sum(num_interactions[i] * lifted_height[i]) < max_interaction_count) logically implies every trace_height_constraint in the child VK. If a child VK has a trace height constraint that isn't implied by the proof shape AIR's check, the recursion circuit wouldn't be able to enforce it, creating a soundness gap. The assertion catches this at circuit construction time.

---

Data flow summary

child_vk.inner.params.logup.max_interaction_count
  │
  ├─► ProofShapeModule.max_interaction_count  (mod.rs:58, 128)
  │     └─► ProofShapeAir.max_interaction_count  (mod.rs:239)
  │           └─► Used in eval() on summary row  (core.rs:1250)
  │                 constrains: total_interactions < max_interaction_count
  │
  ├─► Trace generation (core.rs:414-416)
  │     decompose for diff_idx computation
  │
  ├─► CUDA: ProofShapeTracegenInputs.max_interaction_count  (cuda.rs:33, 115)
  │     └─► fill_summary_row() in air.cu:239,260
  │
  └─► VerifierSubCircuit::new_with_options()  (system/mod.rs:506-514)
        asserts all trace_height_constraints are implied

[jonathanpwang]

I think we should have some more documentation on the exact way we go from the LogUp soundness paper -> LinearConstraints -> what recursion circuit actually bounds