fix: constrain is_valid start value in DeferralCircuitCountAir

[stephenh-axiom-xyz]

Resolves INT-6786.

[github-actions]

Claude finished @stephenh-axiom-xyz's task in 50s —— View job

---

Code Review: PR #2567

• Read changed file and understand context
• Review the fix for correctness and completeness
• Post review feedback

Summary

This PR fixes a soundness bug in DeferralCircuitCountAir where is_valid was not constrained on the first row, allowing a malicious prover to set is_valid = 0 on all rows even when num_deferral_circuits > 0, effectively bypassing the count constraint.

Review

The fix is correct and well-structured. The change splits the is_valid constraints into two cases:

1. num_deferral_circuits > 0: Adds when_first_row().assert_one(local.is_valid) to anchor the start of the valid region, then retains the existing boolean and monotone-decreasing constraints.
2. num_deferral_circuits == 0: Forces is_valid to be zero everywhere with assert_zero(local.is_valid).

Why the old code was broken: Without the first-row constraint, the existing constraints (is_valid ∈ {0,1} and is_valid - next.is_valid ∈ {0,1}) only ensured that is_valid was a non-increasing boolean sequence. A prover could satisfy all constraints by setting is_valid = 0 on every row — the "last row is valid implies row_idx + 1 == n" check (line 79-81) would simply not trigger, and the when_ne transition check (line 76-77) would also pass trivially.

Correctness argument for the fix: With the new first-row assertion:

• When n > 0: is_valid starts at 1 and can only transition from 1→0 once (monotone decreasing boolean). The when_ne constraint forces the transition to happen exactly at row_idx = n - 1, giving exactly n valid rows.
• When n == 0: All rows are forced to have is_valid = 0.

No issues found. The fix is minimal, targeted, and correct.