Add support for more general boundary constraints

[Al-Kindi-0]

Feature description

As it currently stands, the most general type of boundary constraints are of the form $\frac{f(X) - b(X)}{Z(X)}$ where

1. $f(X)$ is the trace column polynomial,
2. $b(X)$ is a polynomial specifying the boundary values enforced on the aforementioned column,
3. $Z(X)$ is a zerofier polynomial on the enforcement domain associated to the boundary constraint. Currently, this is either $X - g^0$ (i.e., first) or $X - g^{-2}$ (i.e., last) where we assume one exemption point and $g$ is the trace domain generator.

However, there are situations where we want to have boundary constraints which involve more than just one trace column, say $f_0(X)$ and $f_1(X)$ and a constraint like $\frac{f_0(X) \cdot f_1(X) - 1}{X - g^{-2}}$.

Why is this feature needed?

This is needed in order to be able to write some constraints where the interaction between components happen through different buses and the consistency of the interactions is enforced through the above kind of boundary constraints.

[bobbinth]

I thought we had a discussion about this somewhere - but I can't seem to find it.

Overall, I think the current IR (i.e., the algebraic graph) should be able to support it. So, the main question is what syntax to use to express this. Another special case here is that, in my understanding, we need this specifically for auxiliary column boundaries (i.e., buses) but not for the main trace constraints (though, I'm sure supporting both wouldn't hurt).

Additionally, since we use two different types of busses, we should make sure that we don't try to "mix" them together.

Off the top of my head, it could look something like:

buses {
    multiset p,
    multiset q,
}

boundary_constraints {
    enf (p, q).first = null;
    enf (p, q).last = null;
}

There may be other, better, ways of doing this though.

[bobbinth]

I think #422 is related to this issue - though a much more radical proposal.

[Al-Kindi-0]

I thought we had a discussion about this somewhere - but I can't seem to find it.

Maybe you are referring to the issue opened in Winterfell.

Overall, I think the current IR (i.e., the algebraic graph) should be able to support it. So, the main question is what syntax to use to express this. Another special case here is that, in my understanding, we need this specifically for auxiliary column boundaries (i.e., buses) but not for the main trace constraints (though, I'm sure supporting both wouldn't hurt).

I can't immediately think of an application in the case of main trace columns but if it is easy to support both then why not.

Additionally, since we use two different types of busses, we should make sure that we don't try to "mix" them together.

Indeed, this is probably the most important "type-safety" check here

Off the top of my head, it could look something like:

buses {
    multiset p,
    multiset q,
}

boundary_constraints {
    enf (p, q).first = null;
    enf (p, q).last = null;
}

There may be other, better, ways of doing this though.

This looks clean and intuitive to me, so +1 from me.

[Al-Kindi-0]

I think #422 is related to this issue - though a much more radical proposal.

Indeed, any solution in this direction will most probably make this issue irrelevant. So, we can put this issue on hold until we discuss further #422.

[Al-Kindi-0]

Given the discussion in #422 and the need for a resolution on the question in this issue in order to conclude the current AirScript milestone, I would like to make the following proposal and get feedback on it as soon as possible.

1. AirScript (backend) can make the following operating assumption, namely that all busses are domain separated. This assumption already holds for the Miden VM constraints though we should double check.
2. For any AIR with interactions, we enforce:
   1. All buses start with 1 (or 0 for LogUp),
   2. 2. All final bus values $p_{i}[final]$, unless explicitly forced to be 1 (or 0 for LogUp) should satisfy the constraint $\pi_i p_{i}[final] = \pi_i \varphi_i$ where $\varphi_i$ is the i-th reduced variable length public inputs group (and similarly for LogUp),
   3. Add constraints to force the claimed values from point 2
3. The prover will include in the proof the (non-trivial) exposed products (sums for LogUp) $p_{i}[final]$, which will be sent in the same round as the Merkle root to the interactions traces i.e., auxiliary segments currently.

The above solution is definitely more work than the solution by @bobbinth , but it seems to me that it includes some of the work that needs to be done anyway on our way to multi-table support (@adr1anh correct me if I am off here) so we might as well expend a bit more effort for a more permanent solution, though I would be also happy with the direct solution by @bobbinth

The crucial thing, however, is to come to a decision quickly, though there is the option of starting the work on the next milestone focused on completing the recursive verifier by writing all constraints and starting only on constraints for the main trace (and not the auxiliary one) while we continue the discussion on this issue and #422

[bobbinth]

I'm wondering if we need to tackle this problem before we tackle the multi-table support. I believe right now we have just a single constraint that we can't express in AirScript, and this constraint is not something that is supported by Winterfell. We could probably leave things as they are for now, and then address this problem once most other things are in place. The overall sequence of actions could be:

1. We finish the remaining frontend tasks - i.e., #423, #440, #444, and maybe a few smaller ones.
2. We start working these in parallel:
   a. Writing existing Miden VM constraint in AirScript.
   b. Building a Plonky3 backend for AirScript. As a part of this, we'd also need to figure out how to address auxiliary trace generation - i.e., do we still keep it in the miden-vm repo, or can we automate it somehow with Plnoky3.
3. We implement multi-table support - the exact approach would need to be finalized in #422.
   a. Depending on the approach taken, we can then revisit this issue.
   b. We will also need to update the Plonky3 backend to handle multiple tables.
4. We update the constraints to make use of multiple tables. My thinking here is that this will not be a radical re-design, but just a small update where we split the execution trace in 2, maybe 3, tables, and these tables will largely look like they do now.
   a. This will also require updates to trace generation, but that's a miden-vm concern.

So, to summarize, I'd probably put this issue on-hold and try to tackle it together with #422.

[Al-Kindi-0]

Fully agree, though should we at least add support for writing these constraints at the front-end level like you described here or should we just leave a TODO when writing bus constraints of this type ?

[bobbinth]

I was thinking we'd just leave a TODO for now as it is not 100% clear if the approach I described is what we'd go with. So, could end up being wasted effort to implement it (even in the frontend).

[Al-Kindi-0]

Makes sense.
@Dominik1999 , I think we have come to a decision regarding this issue, and it can be summarized as putting this issue on hold as it is not a blocker for starting on constraints writing (except for a couple of them) nor for adding the Plonky3 backend. In fact how we solve this last point will influence how we go about closing this issue in the future.

For more details, the relevant comments are here and here