fix: Make Eq3bAir use the correct number of interactions per air

[Golovanov399]

This resolves INT-6828.

Now Eq3bAir propagates the row_idx by the correct amount for each AIR. Note that there is no need for this air to know air_idx or anything other than the number of interactions and the n_lift for this air, so no new columns are added (but we now do the interaction with proof shape air on the last row of the air instead of the first one).

[github-actions]

Claude finished @Golovanov399's task in 1m 52s —— View job

---

Code Review: PR #2558

• Read changed files and surrounding context
• Analyze correctness of the fix
• Post review feedback

---

Summary: This PR adds num_interactions to the Eq3bShapeMessage and moves the shape bus lookup from is_first_in_air to local_is_last (last row of each AIR). This ensures the Eq3b AIR correctly reports the number of interactions per AIR to the proof shape bus, enabling proper verification.

Review

The fix looks correct. Here's my analysis:

1. num_interactions computation (air.rs:281): local.interaction_idx + not(local.has_no_interactions) is correct:

   • When an AIR has interactions: on the last row, interaction_idx is the 0-based index of the last interaction, so adding 1 gives the count.
   • When an AIR has no interactions: interaction_idx = 0 and not(has_no_interactions) = 0, giving num_interactions = 0.

2. Moving lookup to last row (air.rs:283): Using LoopSubAir::local_is_last(...) instead of local.is_first_in_air is necessary because interaction_idx is only known to be the maximum on the last row. On the first row, interaction_idx is always 0 (enforced at line 121), so the old code would always report num_interactions = 1 (or 0 for no-interactions AIRs), regardless of the actual count.

3. .into() conversions (air.rs:278-280): Required because num_interactions is an AB::Expr (a sum), so the message generic T resolves to AB::Expr, and the AB::Var fields need conversion. This is correct.

4. num_interactions.clone() (proof_shape/air.rs:528): Needed because num_interactions is now used in two places (the AirShapeBusMessage at line 528 and the Eq3bShapeMessage at line 985). Previously it was only consumed once. Correct.

5. Proof shape side (proof_shape/air.rs:985): The num_interactions variable here is computed from air_data.num_interactions for each AIR, which is the total interaction count — matching the semantics of what Eq3bAir now sends.

No issues found. The change is minimal, well-scoped, and the bus message fields on both sender and receiver sides are consistent.