Revised bus boundary constraints

This issue describes an alternative implementation of buses which may lead to simplified code generation and verifier implementation. We will assume all our buses are based on logUp, as this is the most natural choice when dealing with multiple tables.

**TLDR**
- Expose a single bus in frontend used for all messages
- Multiple buses can still be supported if necessary, in which case the compiler can inject an additional domain separator at the start of all messages (i.e. the message is `[BUS_ID, m0, m1, ...]`).
- The compiler determines the number of bus columns depending on the desired blowup factor and the degree of the expressions.
- Bus columns are "batched". Each column represents the insertion or removal of multiple queries.
- All bus columns constrain the value in the first row to be 0.
- The prover sends the final logUp value of each bus as part of the proof.
- Each column is constrained in the last row to equal the final value provided by the prover.
- Public input tables no longer need to be treated as variables representing a bus boundary value. The IR still exposes them to facilitate code generation.
- The verifier is responsible for checking that the sum of
- the randomly reduced logUp entries of all public input tables, and
- all the final bus boundary values provided in the proof,
evaluates to zero.

#### Connecting all busses

At the moment, busses by default are independent of one another, unless explicitly connected with a potential `enf busA.last = busB.first` type of syntax. This exposes unnecessary bus implementation details.

Instead, we can assume that all buses are connected, even though they may contain messages used in different contexts. Consider the case where we have two separate buses
- **`range`**: The message `[value]` is a single `Felt` which is sent to the range-check table.
- **`chiplet_op`**: A message `[INSTRUCTION_LABEL, arg0, arg1, ...]` containing an instruction label and a variable number of arguments, which is sent to one of the chiplets.
We can combine these into a single bus by adding the bus name as part of the message, i.e.
- `[RANGE_BUS_LABEL, value]`
- `[CHIPLET_OP_BUS_LABEL, INSTRUCTION_LABEL, arg0, arg1, ...]`
As long as the `*_BUS_LABEL`s are unique, messages from different buses will never collide.

#### Batching buses

Consider a chiplet which enforces `a + b = c`.
```
trace_columns {
main: [
s, // row activation
a, b, c, // arguments
m, // operation multiplicity
],
}

buses {
range,
chip,
}

integrity_constraints {
// row is active or not
enf s^2 = s;

// enforce arguments are u32
range.insert(a) when s;
range.insert(b) when s;
range.insert(c) when s;

// check addition
enf a + b = c when s;

// provide result `m` times
chip.remove(ADD_LABEL, a, b, c) with m;
}
```

This leads to 4 different messages being inserted into/removed from the bus. If we are in a situation where the maximum Air degree is 3 (i.e. with blowup factor 2), then we will need two bus columns to compute the logUp sum.

$$
\begin{aligned}
b^{(0)} =&
\frac{s}{\alpha + \mathsf{RANGE} + \beta \cdot a} +
\frac{s}{\alpha + \mathsf{RANGE} + \beta \cdot b} \\
b^{(1)} =&
\frac{s}{\alpha + \mathsf{RANGE} + \beta \cdot a} + \\
& \frac{m}{\alpha + \mathsf{CHIP} +
\beta \cdot \mathsf{ADD} +
\beta^2 \cdot a +
\beta^3 \cdot b +
\beta^4 \cdot c
}
\end{aligned}
$$

The compiler can figure out the optimal way to pack the columns, taking into account the degrees of the numerator and denominator expressions.

The ability to combine busses is a consequence of dealing with a single bus argument, as we no longer need to consider one column per bus.

In what follows, we will ignore batching for simplicity.

#### Bus boundary constraints

For a bus column $b$ with logUp entries of the form $\frac{m_i}{v_i}$, we have the following first row, transition and last row constraints

$$
\begin{aligned}
b_0 &= 0 \\
b_{i+1} &= b_i + \frac{m_i}{v_i} \\
B &= b_{n-1} + \frac{m_{n-1}}{v_{n-1}}
\end{aligned}
$$

Here, $B$ is the final column value, equal to $\sum_{i=0}^{n-1} \frac{m_i}{v_i}$ which is sent by the prover along with the commitment to the bus column. If there is a single column in the table, we would then instruct the verifier to check that $B=0$ which ensures the integrity of the bus entries.

When dealing with multiple bus columns $b^{(0)}, b^{(1)}, \ldots$ with final values $B^{(0)}, B^{(1)}, \ldots$, the buses are connected by summing the final values. We take $B = B^{(0)} + B^{(1)} + \cdots$ and similarly check that this sum evaluates to zero.

While this does incur a small cost to the verifier, it is possible to integrate this check into the ACE circuit, by adding a virtual (constant) constraint performing this final check.

#### Public Input Table constraints

The main purpose of boundary constraints is to initialize and export an arbitrary number of messages from the bus with values known by the verifier. In the following, we are setting enforcing that the stack starts and ends with specific values, and initialize the kernel with a set of known procedure digests.

```
buses {
proc_hashes,
stack,
}

public_inputs {
stack_inputs: [16],
stack_output: [16],
proc_digests: [[4]]
}

boundary_constraints {
enf proc_hashes.import = proc_digests;
enf stack.import = stack_inputs;
enf stack.export = stack_output;
}
```

Generally, any value specified with `import` would use multiplicity `1`, while `export` values might require either `-1` or an arbitrary multiplicity `m`.

The verifier is responsible for computing for each public input the randomly-reduced logUp term. These are then summed into $$B$$ before checking that it evaluates to 0.

The issue proposes a redesign of bus boundary constraints in the AIR-Script compiler. Start by reading the existing bus implementation in the codebase, likely in the compiler or constraint generation modules. Understand how logUp and bus columns are currently handled. The goal is to implement a single bus system with batched columns, revised boundary constraints, and updated verifier checks. Look for tests related to buses and public inputs to see the expected behavior.

Rédigé par le modèle d'indexation à partir du texte de l'issue.