PublicValuesAir underconstrains tidx across AIR boundaries

[kunxian-xia]

Summary

In ceno_recursion_v2, PublicValuesAir only anchors the first public-value row of each proof to public_values_start_tidx, and only enforces consecutive tidx values while adjacent rows belong to the same AIR. At AIR boundaries, the next row's tidx is not tied to the VK-derived public-value offset.

This leaves non-first AIR public-value transcript indices underconstrained.

Details

Current behavior in src/proof_shape/pvs/air.rs:

• The first public-value row is constrained with local.tidx == public_values_start_tidx.
• For rows in the same AIR, next.tidx == local.tidx + 1 and next.pv_idx == local.pv_idx + 1.
• At an AIR boundary, the AIR only constrains next.is_first_in_air == 1; it does not constrain the new AIR's tidx to the expected start offset or prove the previous AIR had exactly the expected number of public-value rows.

The commented-out NumPublicValuesBus receive indicates this was likely intended to be checked structurally, but it is currently inactive.

Ceno-specific expected behavior

Unlike OpenVM, Ceno stores public values in one global public-value namespace. Each AIR's instance list stores absolute global public-value indices. The recursion circuit then projects those into (air_idx, pv_idx) rows for bus interactions.

A fix should restore a Ceno-adapted NumPublicValuesBus check:

• Proof-shape sends (air_idx, start_tidx, num_pvs) using VK-derived public-value metadata.
• start_tidx = public_values_start_tidx + sum_{j < air_idx} per_air[j].num_public_values.
• num_pvs = per_air[air_idx].num_public_values.
• The sender should be enabled for AIRs with public values in the global public-value block, not gated by trace presence.
• PublicValuesAir receives this message on each AIR's final PV row using tidx = local.tidx - local.pv_idx and num_pvs = local.pv_idx + 1.
• Also constrain is_first_in_air => pv_idx == 0.

This would bind each AIR's public-value row range to the VK-declared global public-value layout and close the AIR-boundary tidx gap.