miden-air 0.25.2

//! Packs four buses into one main-trace lookup column:
//!
//! - Block-stack table: control-flow block nesting.
//! - u32 range-check removes: gated by u32 opcodes.
//! - Log-precompile transcript-state: gated by the log precompile opcode.
//! - Range-table response: always active and isolated in its own group.
//!
//! Opcode-gated interactions share the `main_interactions` group. The range-table response
//! stays in the sibling `range_table` group because it can overlap with them.
//!
//! Main group:
//!   - Block-stack table: JOIN/SPLIT/SPAN/DYN, LOOP, DYNCALL, CALL/SYSCALL, two END cases, RESPAN
//!     batch.
//!   - u32 range-check batch: 4 removes gated by `u32_rc_op`.
//!   - Log-precompile transcript-state batch: 1 remove + 1 add gated by `log_precompile`.
//!
//! Sibling group:
//!   - Range-table response: a single insert with runtime multiplicity `range_m`. It lives in its
//!     own group because it overlaps with every opcode-gated interaction above.
//!
//! The `main_interactions` group is mutually exclusive by opcode:
//!
//! - Block-stack: {JOIN, SPLIT, SPAN, DYN, LOOP, DYNCALL, CALL, SYSCALL, END, RESPAN}
//! - u32: {U32SPLIT, U32ASSERT2, U32ADD, U32SUB, U32MUL, U32DIV, U32MOD, U32AND, U32XOR, U32ADD3,
//!   U32MADD, ...}. These are `prefix_100` in the opcode encoding.
//! - LOGPRECOMPILE: {LOGPRECOMPILE}.
//!
//! No row can fire two of these simultaneously. The END-simple / END-call/syscall split
//! inside block-stack is mutually exclusive via the `is_call + is_syscall ≤ 1` end-flag
//! invariant.
//!
//! Degree budget:
//!
//! | Interaction | Gate deg | Payload | U | V |
//! |---|---|---|---|---|
//! | JOIN/SPLIT/SPAN/DYN simple add | 5 | Simple, denom 1 | 6 | 5 |
//! | LOOP simple add | 5 | Simple, denom 1 | 6 | 5 |
//! | DYNCALL simple add (Full msg) | 5 | Full, denom 1 | 6 | 5 |
//! | CALL/SYSCALL simple add (Full msg) | 4 | Full, denom 1 | 5 | 4 |
//! | END simple remove | 5 | Simple, denom 1 | 6 | 5 |
//! | END call/syscall remove (Full msg) | 5 | Full, denom 1 | 6 | 5 |
//! | RESPAN batch (k=2, f=respan deg 4) | n/a | Simple | 6 | 5 |
//! | u32rc batch (k=4, f=u32_rc_op deg 3) | n/a | Range, denom 1 | 7 | 6 |
//! | logpre batch (k=2, f=log_precompile deg 5) | n/a | LogPrecompile, denom 1 | 7 | 6 |
//!
//! Main group max: `U_g = 7, V_g = 6`.
//!
//! Sibling range-table group: `g.insert(ONE, range_m, RangeMsg)`. Gate deg 0, mult deg 1,
//! denom deg 1. `U_g = 1, V_g = 1`.
//!
//! Column fold (cross-mul rule `U_col = ∏ U_gi`, `V_col = Σᵢ V_gi · ∏_{j≠i} U_gj`):
//!
//! - `deg(U_col) = 7 + 1 = 8`
//! - `deg(V_col) = max(6 + 1, 1 + 7) = 8`
//! - Transition = `max(1 + 8, 8) = 9`, 0 headroom.

use core::array;

use miden_core::field::PrimeCharacteristicRing;

use crate::{
    constraints::lookup::{
        main_air::{MainBusContext, MainLookupBuilder},
        messages::{BlockStackMsg, LogPrecompileMsg, RangeMsg},
    },
    lookup::{Deg, LookupBatch, LookupColumn, LookupGroup},
    trace::log_precompile::{HELPER_STATE_PREV_RANGE, STACK_STATE_NEW_RANGE},
};

/// Upper bound on fractions this emitter pushes into its column per row.
///
/// Main group per-row max is `max(1, 1, 1, 1, 1, 1, 2 (RESPAN), 4 (u32rc), 2 (logpre)) = 4`
/// The u32rc 4-remove batch is the largest branch.
/// Sibling range-table group always contributes 1 fraction.
/// Both groups run unconditionally (the main group fires at most one branch per row but
/// the per-column accumulator allocates the worst-case slot budget), so the per-row max is
/// the sum: `4 + 1 = 5`.
pub(in crate::constraints::lookup) const MAX_INTERACTIONS_PER_ROW: usize = 5;

/// Emit the merged block-stack + u32rc + logpre + range-table column.
pub(in crate::constraints::lookup) fn emit_block_stack_and_range_logcap<LB>(
    builder: &mut LB,
    ctx: &MainBusContext<LB>,
) where
    LB: MainLookupBuilder,
{
    let local = ctx.local;
    let next = ctx.next;
    let op_flags = &ctx.op_flags;

    let dec = &local.decoder;
    let dec_next = &next.decoder;
    let stk = &local.stack;
    let stk_next = &next.stack;

    // ---- Block-stack captures (from block_stack.rs) ----
    //
    // `dec.hasher_state` holds `[h0..h7]` with `h[4..8]` doubling as the end-block flags
    // (see `end_block_flags()`). DYNCALL reads `h[4]`/`h[5]` as `fmp`/`depth`; the END
    // variants read `is_loop`/`is_call`/`is_syscall` through the typed `EndBlockFlags`
    // overlay.
    let addr = dec.addr;
    let addr_next = dec_next.addr;
    let h4 = dec.hasher_state[4];
    let h5 = dec.hasher_state[5];
    let h1_next = dec_next.hasher_state[1];
    let end_flags = dec.end_block_flags();

    let b0 = stk.b0;
    let b1 = stk.b1;
    let b0_next = stk_next.b0;
    let b1_next = stk_next.b1;

    let sys_ctx = local.system.ctx;
    let sys_ctx_next = next.system.ctx;

    let fn_hash = local.system.fn_hash;
    let fn_hash_next = next.system.fn_hash;

    let range_m = local.range.multiplicity;
    let range_v = local.range.value;

    // ---- u32rc + logpre captures (from range_logcap.rs) ----

    let user_helpers = dec.user_op_helpers();
    let f_u32rc = op_flags.u32_rc_op();
    let f_log_precompile = op_flags.log_precompile();

    // u32rc helpers: first 4 of the 6 user_op_helpers.
    let u32rc_helpers: [LB::Var; 4] = array::from_fn(|i| user_helpers[i]);

    // LOGPRECOMPILE transcript-state add/remove payloads.
    let state_prev: [LB::Var; 4] =
        array::from_fn(|i| user_helpers[HELPER_STATE_PREV_RANGE.start + i]);
    let state_new: [LB::Var; 4] = array::from_fn(|i| stk_next.get(STACK_STATE_NEW_RANGE.start + i));

    builder.next_column(
        |col| {
            // ──────────── Main group: all opcode-gated interactions ────────────
            col.group(
                "main_interactions",
                |g| {
                    // ---- Block-stack table (BusId::BlockStackTable) ----

                    // JOIN/SPLIT/SPAN/DYN: simple push with `is_loop = 0`.
                    let f =
                        op_flags.join() + op_flags.split() + op_flags.span() + op_flags.dyn_op();
                    g.add(
                        "join_split_span_dyn",
                        f,
                        || {
                            let block_id = addr_next.into();
                            let parent_id = addr.into();
                            let is_loop = LB::Expr::ZERO;
                            BlockStackMsg::Simple { block_id, parent_id, is_loop }
                        },
                        Deg { v: 5, u: 6 },
                    );

                    // LOOP: push with `is_loop = 1`. Under do-while semantics LOOP reads no
                    // stack input, as it unconditionally enters the loop.
                    g.add(
                        "loop",
                        op_flags.loop_op(),
                        || {
                            let block_id = addr_next.into();
                            let parent_id = addr.into();
                            let is_loop = LB::Expr::ONE;
                            BlockStackMsg::Simple { block_id, parent_id, is_loop }
                        },
                        Deg { v: 5, u: 6 },
                    );

                    // DYNCALL: full push with h[4]/h[5] as fmp/depth.
                    g.add(
                        "dyncall",
                        op_flags.dyncall(),
                        || {
                            let block_id = addr_next.into();
                            let parent_id = addr.into();
                            let is_loop = LB::Expr::ZERO;
                            let ctx = sys_ctx.into();
                            let fmp = h4.into();
                            let depth = h5.into();
                            let fn_hash = fn_hash.map(LB::Expr::from);
                            BlockStackMsg::Full {
                                block_id,
                                parent_id,
                                is_loop,
                                ctx,
                                fmp,
                                depth,
                                fn_hash,
                            }
                        },
                        Deg { v: 5, u: 6 },
                    );

                    // CALL/SYSCALL: full push saving the caller context.
                    let f = op_flags.call() + op_flags.syscall();
                    g.add(
                        "call_syscall",
                        f,
                        || {
                            let block_id = addr_next.into();
                            let parent_id = addr.into();
                            let is_loop = LB::Expr::ZERO;
                            let ctx = sys_ctx.into();
                            let fmp = b0.into();
                            let depth = b1.into();
                            let fn_hash = fn_hash.map(LB::Expr::from);
                            BlockStackMsg::Full {
                                block_id,
                                parent_id,
                                is_loop,
                                ctx,
                                fmp,
                                depth,
                                fn_hash,
                            }
                        },
                        Deg { v: 4, u: 5 },
                    );

                    // END (simple blocks): pop with the stored is_loop.
                    let f = op_flags.end()
                        * (LB::Expr::ONE - end_flags.is_call.into() - end_flags.is_syscall.into());
                    g.remove(
                        "end_simple",
                        f,
                        || {
                            let block_id = addr.into();
                            let parent_id = addr_next.into();
                            let is_loop = end_flags.is_loop.into();
                            BlockStackMsg::Simple { block_id, parent_id, is_loop }
                        },
                        Deg { v: 5, u: 6 },
                    );

                    // END (after CALL/SYSCALL): pop with restored caller context.
                    let f =
                        op_flags.end() * (end_flags.is_call.into() + end_flags.is_syscall.into());
                    g.remove(
                        "end_call_syscall",
                        f,
                        || {
                            let block_id = addr.into();
                            let parent_id = addr_next.into();
                            let is_loop = end_flags.is_loop.into();
                            let ctx = sys_ctx_next.into();
                            let fmp = b0_next.into();
                            let depth = b1_next.into();
                            let fn_hash = fn_hash_next.map(LB::Expr::from);
                            BlockStackMsg::Full {
                                block_id,
                                parent_id,
                                is_loop,
                                ctx,
                                fmp,
                                depth,
                                fn_hash,
                            }
                        },
                        Deg { v: 5, u: 6 },
                    );

                    // RESPAN: simultaneous push + pop — one batch under the RESPAN flag.
                    g.batch(
                        "respan",
                        op_flags.respan(),
                        |b| {
                            let block_id_add = addr_next.into();
                            let parent_id_add = h1_next.into();
                            let is_loop_add = LB::Expr::ZERO;
                            b.add(
                                "respan_add",
                                BlockStackMsg::Simple {
                                    block_id: block_id_add,
                                    parent_id: parent_id_add,
                                    is_loop: is_loop_add,
                                },
                                Deg { v: 4, u: 5 },
                            );
                            let block_id_rem = addr.into();
                            let parent_id_rem = h1_next.into();
                            let is_loop_rem = LB::Expr::ZERO;
                            b.remove(
                                "respan_remove",
                                BlockStackMsg::Simple {
                                    block_id: block_id_rem,
                                    parent_id: parent_id_rem,
                                    is_loop: is_loop_rem,
                                },
                                Deg { v: 4, u: 5 },
                            );
                        },
                        Deg { v: 5, u: 6 }, // (V, U) = (1 + 4, 2 + 4)
                    );

                    // ---- u32 range-check removes (BusId::RangeCheck) ----
                    // Four simultaneous range-check removals under the u32rc flag. Mutually
                    // exclusive with all block-stack branches (u32 ops are disjoint from
                    // control-flow ops) and with logpre (disjoint from LOGPRECOMPILE).
                    g.batch(
                        "u32_range_check",
                        f_u32rc,
                        move |b| {
                            for helper in u32rc_helpers {
                                let value = helper.into();
                                b.remove("u32rc_remove", RangeMsg { value }, Deg { v: 3, u: 4 });
                            }
                        },
                        Deg { v: 6, u: 7 }, // (V, U) = (3 + 3, 4 + 3)
                    );

                    // ---- Log-precompile transcript-state update (BusId::LogPrecompileTranscript)
                    // ---- Remove the previous transcript state, add the next. Mutually
                    // exclusive with all block-stack branches and with u32rc.
                    g.batch(
                        "log_precompile_state",
                        f_log_precompile,
                        move |b| {
                            let state_prev_expr = state_prev.map(LB::Expr::from);
                            b.remove(
                                "logpre_state_remove",
                                LogPrecompileMsg { state: state_prev_expr },
                                Deg { v: 5, u: 6 },
                            );
                            let state_new_expr = state_new.map(LB::Expr::from);
                            b.add(
                                "logpre_state_add",
                                LogPrecompileMsg { state: state_new_expr },
                                Deg { v: 5, u: 6 },
                            );
                        },
                        Deg { v: 6, u: 7 }, // (V, U) = (1 + 5, 2 + 5)
                    );
                },
                Deg { v: 6, u: 7 },
            );

            // The range-table response is always active, so it must remain separate from the
            // opcode-gated main group. On the padding row this still contributes zero because
            // `range_m` is zero, preserving the no-interactions-on-last-row invariant.
            col.group(
                "range_table",
                |g| {
                    g.insert(
                        "range_response",
                        LB::Expr::ONE,
                        range_m.into(),
                        || {
                            let value = range_v.into();
                            RangeMsg { value }
                        },
                        Deg { v: 1, u: 1 },
                    );
                },
                Deg { v: 1, u: 1 },
            );
        },
        Deg { v: 8, u: 8 },
    );
}