fix: make Eq3bAir receive n_logup and n_lift

[Golovanov399]

This resolves INT-6774.

Eq3bAir now maintains n_logup as well, constrains that it's constant across the AIR as well as n_lift and receives them one per AIR.

[stephenh-axiom-xyz]

LGTM after some nits + CUDA tracegen

[stephenh-axiom-xyz]

This should be local.is_valid + local.is_last

[Golovanov399]

-?

[Golovanov399]

Ah no, it should be is_valid + is_last - is_last, so now is right

[github-actions]

Claude finished @Golovanov399's task in 2m 20s —— View job

---

Code Review: Make Eq3bAir receive n_logup and n_lift

• Gather context and read changed files
• Review constraint correctness and bus wiring
• Review trace generation (CPU + CUDA)
• Post review findings

---

Summary

This PR adds an Eq3bShapeBus to cryptographically constrain n_lift and n_logup per AIR within Eq3bAir, replacing a trust-based approach. The changes span bus definition, AIR constraints, CPU + CUDA trace generation, and module wiring.

Constraint Correctness

The constraint logic is sound:

1. n_lift constancy (eq_3b/air.rs:140-141): Constrained within_one_air — correct since n_lift is per-AIR.

2. n_logup constancy (eq_3b/air.rs:143-147): Uses LoopSubAir::local_is_transition(next.is_valid, next.is_first) to enforce constancy across all transitions within the same proof. Correct scope since n_logup is a proof-level value.

3. n_logup value constraint (eq_3b/air.rs:189-191): local.n == local.n_logup on last row of each interaction, gated by not(has_no_interactions). Since n is 0-indexed and increments by 1, this asserts each interaction has exactly n_logup + 1 rows.

4. Bus lookup (eq_3b/air.rs:274-283): Fires on is_first_in_air, sending (sort_idx, n_lift, n_logup). Each AIR contributes exactly one lookup — for AIRs with interactions via interaction_idx == 0 && n == 0, and for dummy AIRs via the has_no_interactions => is_first_in_air constraint.

5. ProofShapeAir provider (proof_shape/air.rs:978-987): add_key_with_lookups fires with local.is_present count (one per present AIR), matching the one-lookup-per-AIR on the Eq3b side. The n_lift computation at lines 967-968 correctly computes max(0, log_height - l_skip) via (log_height - l_skip) * (1 - n_sign_bit), matching the saturating_sub in trace generation.

6. n_logup constancy in ProofShapeAir (proof_shape/air.rs:243-244): when(local.is_valid).assert_eq(local.n_logup, next.n_logup) — this correctly chains n_logup across all valid rows and into the summary row (since the last valid row's next is the summary row, and the constraint fires because local.is_valid = 1).

Trace Generation

• CPU trace gen (eq_3b/trace.rs:200): Sets cols.n_logup = F::from_usize(n_logup) on every row. Correct.
• ProofShapeAir CPU trace gen (proof_shape/trace.rs): Sets n_logup on present rows (line 117), non-present rows (line 221), and summary rows (line 325). All consistent.

CUDA Synchronization

• eq_3b.cu:21: n_logup field added between n_lift and two_to_the_n_lift, matching the Rust Eq3bColumns struct layout.
• proof_shape/air.cu:63: n_logup field position matches the Rust ProofShapeCols struct.

Module Wiring

• Eq3bShapeBus and Eq3bShapeMessage properly defined in bus.rs:663-669 using define_typed_per_proof_lookup_bus!.
• Bus threaded through BusInventory (system/mod.rs:233), BatchConstraintModule (batch_constraint/mod.rs), ProofShapeModule (proof_shape/mod.rs:257), and Eq3bAir construction.

Reviewer Nit Status

The latest commits addressed the reviewer's nits:

• Extracted n_lift into a shared variable at proof_shape/air.rs:967-968.
• Removed the starting_cidx == n_logup alias on the summary row.

Verdict

LGTM. The bus wiring is complete, constraints are correct, and trace generation is consistent between CPU and CUDA. No issues found.

---